[<<][staapl][>>][..]

Thu Jul 16 11:37:15 CEST 2009

## curry-howard correspondence

I have a chance here to understand some theory better. Type systems
are simplified semantics: The morphism between typed programs and
proofs is a well-specified version of simplification.
In Pierce 9.4 p.109:
linear logic <-> linear types
modal logic <-> partial evaluation and run-time code gen
I did not know this for modal logic[1]. Probably a point to expand on
a bit..
[1] http://en.wikipedia.org/wiki/Modal_logic

[Reply][About]

[<<][staapl][>>][..]