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