Thu Jul 16 11:37:15 CEST 2009
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. Probably a point to expand on