Proof nets and the λ-calculus
2001
https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=a9171ccd4d4a64ebf417fd9680d487c37057db93
proof nets
lambda calculus
linear logic
MELL
cut elimination
Curry-Howard
/icons/hr.icon
description
MELL は単純型付きラムダ計算とカリーハワード同型だから，MELLのProof Netsで単純型付きラムダ計算(の型導出木)が書ける．