LFMTP 2010 Accepted Papers

Pattern Unification for the Lambda Calculus with Linear and Affine Types
Generating Bijections between HOAS and the Natural  Numbers
Closed nominal rewriting and efficiently computable nominal algebra equality
Pure Type Systems without Explicit Contexts
Explicit substitutions for contextual type theory
A Monadic Formalization of ML5
Representing Isabelle in LF