Adam Chlipala
ABSTRACT
We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.
Supplemental Material
Available for Download
Slides from the presentation
Supplemental material for: Parametric higher-order abstract syntax for mechanized semantics
- Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proc. TLCA, pages 13--28, 1993. Google Scholar
Digital Library
- Simon Ambler, Roy L. Crole, and Alberto Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In Proc. TPHOLs, pages 13--30, 2002. Google ScholarDigital Library
- Brian Aydemir, Arthur Chargu´eraud, Benjamin C. Pierce, Randy Pollack, and StephanieWeirich. Engineering formal metatheory. In Proc. POPL, pages 3--15, 2008. Google ScholarDigital Library
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The PoplMark challenge. In Proc. TPHOLs, pages 50--65, 2005. Google ScholarDigital Library
- Eli Barzilay and Stuart F. Allen. Reflecting higher-order abstract syntax in Nuprl. In Proc. TPHOLs (Track B), pages 23--32, 2002.Google Scholar
- Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004. Google ScholarDigital Library
- Anna Bucalo, Furio Honsell, Marino Miculan, Ivan Scagnetto, and Martin Hofmann. Consistency of the theory of contexts. J. Funct. Program., 16 (3): 327--372, 2006. Google ScholarDigital Library
- Venanzio Capretta and Amy P. Felty. Combining de Bruijn indices and higher-order abstract syntax in Coq. In Proc. TYPES, pages 63--77, 2006. Google ScholarDigital Library
- Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In Proc. PLDI, pages 54--65, 2007. Google ScholarDigital Library
- Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Proc. LPAR, pages 211--225, 2007. Google ScholarDigital Library
- Maulik A. Dave. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes, 28 (6): 2--2, 2003. Google ScholarDigital Library
- Nicolas G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5): 381--392, 1972.Google ScholarCross Ref
- David Delahaye. A tactic language for the system Coq. In Proc. LPAR, pages 85--95, 2000. Google ScholarDigital Library
- Joëlle Despeyroux, Amy P. Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In Proc. TLCA, pages 124--138, 1995. Google ScholarDigital Library
- Leonidas Fegaras and Tim Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In Proc. POPL, pages 284--294, 1996. Google ScholarDigital Library
- Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In Proc. ICFP, 2008. Google ScholarDigital Library
- Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proc. POPL, pages 206--219, 1993. Google ScholarDigital Library
- Robert Harper and Christopher Stone. A type-theoretic interpretation of Standard ML. In Proof, language, and interaction: essays in honour of Robin Milner, pages 341--387, 2000. Google ScholarDigital Library
- Jason Hickey, Aleksey Nogin, Xin Yu, and Alexei Kopylov. Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection. In Proc. ICFP, pages 172--183, 2006. Google ScholarDigital Library
- Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Proc. LICS, pages 204--213, 1999. Google ScholarDigital Library
- Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In Proc. ICALP, pages 963--978, 2001. Google ScholarDigital Library
- Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, pages 42--54, 2006. Google ScholarDigital Library
- James Mckinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reason., 23 (3): 373--409, 1999. Google ScholarDigital Library
- Yasuhiko Minamide and Koji Okuma. Verifying CPS transformations in Isabelle/HOL. In Proc. MERLIN, pages 1--8, 2003. Google ScholarDigital Library
- J. Strother Moore. A mechanically verified language implementation. J. Automated Reasoning, 5 (4): 461--492, 1989. Google ScholarDigital Library
- L. C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828: xvii + 321, 1994.Google Scholar
- F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proc. PLDI, pages 199--208, 1988. Google ScholarDigital Library
- Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Proc. CADE, pages 202--206, 1999. Google ScholarDigital Library
- Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Proc. POPL, pages 371--382, 2008. Google ScholarDigital Library
- Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266: 1--57, 2001. Google ScholarDigital Library
- Ye Henry Tian. Mechanically verifying correctness of CPS compilation. In Proc. CATS, pages 41--51, 2006. Google ScholarDigital Library
- Valery Trifonov, Bratin Saha, and Zhong Shao. Fully reflexive intensional type analysis. In Proc. ICFP, pages 82--93, 2000. Google ScholarDigital Library
- C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In Proc. CADE, pages 38--53, 2005. Google ScholarDigital Library
- Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program., 18 (1): 87--140, 2008. Google ScholarDigital Library
Index Terms
- Parametric higher-order abstract syntax for mechanized semantics
Recommendations
Parametric higher-order abstract syntax for mechanized semantics
ICFP '08We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's ...
A certified type-preserving compiler from lambda calculus to assembly language
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler ...
A certified type-preserving compiler from lambda calculus to assembly language
Proceedings of the 2007 PLDI conferenceWe present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler ...
Comments