Parametric higher-order abstract syntax for mechanized semantics. (English) Zbl 1323.68184
Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20–28, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-919-7). ACM SIGPLAN Notices 43, No. 9, 143-156 (2008).
MSC:
| 68N20 | Theory of compilers and interpreters |
| 68N15 | Theory of programming languages |
| 68N18 | Functional programming and lambda calculus |
| 68Q55 | Semantics in the theory of computing |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Keywords:
compiler verification; dependent types; interactive proof assistants; type-theoretic semanticsReferences:
| [1] | Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proc. TLCA, pages 13-28, 1993. · Zbl 0797.68095 |
| [2] | 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. · Zbl 1013.68545 |
| [3] | Brian Aydemir, Arthur Chargu´eraud, Benjamin C. Pierce, Randy Pollack, and StephanieWeirich. Engineering formal metatheory. In Proc. POPL, pages 3-15, 2008. 10.1145/1328438.1328443 · Zbl 1295.68052 |
| [4] | 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. 10.1007/11541868_4 · Zbl 1152.68516 |
| [5] | Eli Barzilay and Stuart F. Allen. Reflecting higher-order abstract syntax in Nuprl. In Proc. TPHOLs (Track B), pages 23-32, 2002. |
| [6] | 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. · Zbl 1069.68095 |
| [7] | 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. 10.1017/S0956796806005892 · Zbl 1092.68022 |
| [8] | Venanzio Capretta and Amy P. Felty. Combining de Bruijn indices and higher-order abstract syntax in Coq. In Proc. TYPES, pages 63-77, 2006. · Zbl 1178.68525 |
| [9] | Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In Proc. PLDI, pages 54-65, 2007. 10.1145/1250734.1250742 |
| [10] | Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Proc. LPAR, pages 211-225, 2007. · Zbl 1137.68345 |
| [11] | Maulik A. Dave. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes, 28 (6): 2-2, 2003. 10.1145/966221.966235 |
| [12] | 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. · Zbl 0253.68007 |
| [13] | David Delahaye. A tactic language for the system Coq. In Proc. LPAR, pages 85-95, 2000. · Zbl 0988.68584 |
| [14] | Joëlle Despeyroux, Amy P. Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In Proc. TLCA, pages 124-138, 1995. · Zbl 1063.68650 |
| [15] | Leonidas Fegaras and Tim Sheard. Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space). In Proc. POPL, pages 284-294, 1996. 10.1145/237721.237792 |
| [16] | Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In Proc. ICFP, 2008. 10.1145/1411204.1411218 |
| [17] | Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proc. POPL, pages 206-219, 1993. 10.1145/158511.158630 |
| [18] | 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. |
| [19] | 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. 10.1145/1159803.1159826 · Zbl 1321.68194 |
| [20] | Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Proc. LICS, pages 204-213, 1999. |
| [21] | Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In Proc. ICALP, pages 963-978, 2001. · Zbl 0986.68016 |
| [22] | Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, pages 42-54, 2006. 10.1145/1111037.1111042 · Zbl 1369.68124 |
| [23] | James Mckinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reason., 23 (3): 373-409, 1999. 10.1023/A:1006294005493 · Zbl 0940.03019 |
| [24] | Yasuhiko Minamide and Koji Okuma. Verifying CPS transformations in Isabelle/HOL. In Proc. MERLIN, pages 1-8, 2003. 10.1145/976571.976576 |
| [25] | J. Strother Moore. A mechanically verified language implementation. J. Automated Reasoning, 5 (4): 461-492, 1989. |
| [26] | L. C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828: xvii + 321, 1994. · Zbl 0825.68059 |
| [27] | F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proc. PLDI, pages 199-208, 1988. 10.1145/53990.54010 |
| [28] | Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Proc. CADE, pages 202-206, 1999. |
| [29] | Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Proc. POPL, pages 371-382, 2008. 10.1145/1328438.1328483 · Zbl 1295.68068 |
| [30] | Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266: 1-57, 2001. 10.1016/S0304-3975(00)00418-7 · Zbl 0994.68028 |
| [31] | Ye Henry Tian. Mechanically verifying correctness of CPS compilation. In Proc. CATS, pages 41-51, 2006. |
| [32] | Valery Trifonov, Bratin Saha, and Zhong Shao. Fully reflexive intensional type analysis. In Proc. ICFP, pages 82-93, 2000. 10.1145/351240.351248 · Zbl 1321.68176 |
| [33] | C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In Proc. CADE, pages 38-53, 2005. 10.1007/11532231_4 · Zbl 1135.68561 |
| [34] | Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program., 18 (1): 87-140, 2008. 10.1017/S0956796807006557 · Zbl 1128.68021 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
