Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.

Christine Rckl, Daniel Hirschkoff, Stefan Berghofer

Browse the full FOSSACS paper archive.