Lambda the Ultimate

Natural Deduction for Intuitionistic Non-Commutative Linear Logic, Jeff Polakow and Frank Pfenning. TLCA 1999.

Intuitionistic logic captures functional programming in a logical way, as can be seen from the Curry-Howard isomorphism between constructive proofs and functional programs. However, there are many structural properties of programs that are not captured within the intuitionistic framework, such as resource usage, computational complexity, and sequentiality. Intuitionistic linear logic can be thought of as a refinement of intuitionistic logic in which the resource consumption properties of functions can be expressed internally. Here, we further refine it to allow the expression of sequencing of computations. We achieve this by controlling the use of the structural rule of exchange to arrive at intuitionistic non-commutative linear logic.

My earlier post on linguistics reminded me of the Lambek calculus, which is an ordered logic invented in 1958(!) to model how to parse sentences. So I wanted to find a paper on ordered logic (ie, you can't freely swap the order of hypotheses in a context) and link to that.