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