LOLA 2010 Accepted Papers

An Affine-Intuitionistic System of Types and Effects: Confluence and Termination
Full abstraction in a metalanguage for state
Machine code: architecture-independent formal verification and proof-producing compilation
Fullness of monadic translation by TT-lifting
Step-Indexing: The Good, the Bad and the Ugly
A deeper understanding of the deep frame axiom (extended abstract)
On the Role of Interaction in Implicit Computational Complexity
Krivine realizability for compiler correctness