research-article

Parametric higher-order abstract syntax for mechanized semantics

Author:

Adam ChlipalaAuthors Info & Claims

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

Pages 143 - 156

https://doi.org/10.1145/1411204.1411226

Published: 20 September 2008 Publication History

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.

Supplementary Material

JPG File (1411226.jpg)

Download
14.40 KB

index.html (index.html)

Slides from the presentation

Download
.99 KB

ZIP File (p143-slides.zip)

Supplemental material for: Parametric higher-order abstract syntax for mechanized semantics

Download
10.30 MB

Audio only (1411226.mp3)

Download
9.05 MB

Video (1411226.mp4)

Download
124.82 MB

References

[1]

Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proc. TLCA, pages 13--28, 1993.

Digital Library

[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.

Digital Library

[3]

Brian Aydemir, Arthur Chargu´eraud, Benjamin C. Pierce, Randy Pollack, and StephanieWeirich. Engineering formal metatheory. In Proc. POPL, pages 3--15, 2008.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[9]

Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In Proc. PLDI, pages 54--65, 2007.

Digital Library

[10]

Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Proc. LPAR, pages 211--225, 2007.

Digital Library

[11]

Maulik A. Dave. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes, 28 (6): 2--2, 2003.

Digital Library

[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.

[13]

David Delahaye. A tactic language for the system Coq. In Proc. LPAR, pages 85--95, 2000.

Digital Library

[14]

Joëlle Despeyroux, Amy P. Felty, and André Hirschowitz. Higher-order abstract syntax in Coq. In Proc. TLCA, pages 124--138, 1995.

Digital Library

[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.

Digital Library

[16]

Louis-Julien Guillemette and Stefan Monnier. A type-preserving compiler in Haskell. In Proc. ICFP, 2008.

Digital Library

[17]

Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proc. POPL, pages 206--219, 1993.

Digital Library

[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.

Digital Library

[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.

Digital Library

[20]

Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Proc. LICS, pages 204--213, 1999.

Digital Library

[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.

Digital Library

[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.

Digital Library

[23]

James Mckinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reason., 23 (3): 373--409, 1999.

Digital Library

[24]

Yasuhiko Minamide and Koji Okuma. Verifying CPS transformations in Isabelle/HOL. In Proc. MERLIN, pages 1--8, 2003.

Digital Library

[25]

J. Strother Moore. A mechanically verified language implementation. J. Automated Reasoning, 5 (4): 461--492, 1989.

Digital Library

[26]

L. C. Paulson. Isabelle: A generic theorem prover. Lecture Notes in Computer Science, 828: xvii + 321, 1994.

[27]

F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proc. PLDI, pages 199--208, 1988.

Digital Library

[28]

Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Proc. CADE, pages 202--206, 1999.

Digital Library

[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.

Digital Library

[30]

Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266: 1--57, 2001.

Digital Library

[31]

Ye Henry Tian. Mechanically verifying correctness of CPS compilation. In Proc. CATS, pages 41--51, 2006.

Digital Library

[32]

Valery Trifonov, Bratin Saha, and Zhong Shao. Fully reflexive intensional type analysis. In Proc. ICFP, pages 82--93, 2000.

Digital Library

[33]

C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In Proc. CADE, pages 38--53, 2005.

Digital Library

[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.

Digital Library

Cited By

Bahr PHutton G(2024)Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746388:ICFP(370-394)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674638
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Popescu A(2024)Nominal Recursors as Epi-RecursorsProceedings of the ACM on Programming Languages10.1145/36328578:POPL(425-456)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632857
Show More Cited By

Recommendations

Parametric higher-order abstract syntax for mechanized semantics
ICFP '08

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 ...
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 Implementation

We 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 conference

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programming

September 2008

422 pages

ISBN:9781595939197

DOI:10.1145/1411204

General Chair:
James Hook
Portland State University, USA
,
Program Chair:
Peter Thiemann
Universität Freiburg, Germany

ACM SIGPLAN Notices Volume 43, Issue 9
ICFP '08
September 2008
399 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1411203
Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 September 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP08

Sponsor:

ICFP08: ACM SIGPLAN International Conference on Functional Programming

September 20 - 28, 2008

BC, Victoria, Canada

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

154
Total Citations
View Citations
769
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)10

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bahr PHutton G(2024)Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36746388:ICFP(370-394)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674638
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Popescu A(2024)Nominal Recursors as Epi-RecursorsProceedings of the ACM on Programming Languages10.1145/36328578:POPL(425-456)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632857
Gross JErbsen APhilipoom JAgrawal RChlipala A(2024)Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for CoqJournal of Automated Reasoning10.1007/s10817-024-09705-668:3Online publication date: 14-Aug-2024
https://doi.org/10.1007/s10817-024-09705-6
Ni YWang Y(2024)Generic Reasoning of the Locally Nameless RepresentationProgramming Languages and Systems10.1007/978-981-97-8943-6_3(42-62)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_3
Dunn LTannen VZdancewic S(2023)Syntax Monads for the Working Formal MetatheoristElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.7397(98-117)Online publication date: 14-Dec-2023
https://doi.org/10.4204/EPTCS.397.7
Mell SBastani OZdancewic S(2023)Ideograph: A Language for Expressing and Manipulating Structured DataElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.377.4377(65-84)Online publication date: 1-Apr-2023
https://doi.org/10.4204/EPTCS.377.4
Sano CKavanagh RPientka B(2023)Mechanizing Session-Types using a Structural View: Enforcing Linearity without LinearityProceedings of the ACM on Programming Languages10.1145/36228107:OOPSLA2(374-399)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622810
Koopman PLubbers M(2023)Strongly-Typed Multi-View Stack-Based ComputationsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610623(1-12)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610623
Matsuda KFrohlich SWang MWu N(2023)Embedding by UnembeddingProceedings of the ACM on Programming Languages10.1145/36078307:ICFP(1-47)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607830
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents