Session 8

LJ, LJT & LJTPCF calculi

• Herbelin, "A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure"
• Herbelin, "Séquents qu’on calcule"
• Cervesato, Pfenning, "A Linear Spine Calculus"
• Herbelin, "A sequent calculus presentation of the Calculus of Inductive Constructions (work in progress)"