skip to main content
research-article

Meta-theory à la carte

Published: 23 January 2013 Publication History

Abstract

Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results.
The key contribution of this paper is the development of an induction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components. This framework enables a more structured approach to the reuse of meta-theory formalizations through the composition of modular inductive definitions and proofs.
Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages.

Supplementary Material

JPG File (r2d1_talk7.jpg)
MP4 File (r2d1_talk7.mp4)

References

[1]
B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering Formal Metatheory. In POPL'08, 2008.
[2]
B. E. Aydemir and S. Weirich. LNgen: Tool Support for Locally Nameless Representations, 2009. Unpublished manuscript.
[3]
B.E. Aydemir et al. Mechanized Metatheory for the Masses: The PoplMark Challenge. In TPHOLs'05, 2005.
[4]
P. Bahr. Evaluation `a la carte: Non-strict evaluation via compositional data types. In Proceedings of the 23rd Nordic Workshop on Programming Theory, NWPT '11, pages 38--40, 2011.
[5]
D. Batory, J. Kim, and P. Höfner. Feature interactions, products, and composition. In GPCE, 2011.
[6]
C. Böhm and A. Berarducci. Automatic synthesis of typed lambdaprograms on term algebras. Theor. Comput. Sci., 39, 1985.
[7]
O. Boite. Proof reuse with extended inductive types. In Theorem Proving in Higher Order Logics, pages 50--65, 2004.
[8]
A. Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In ICFP'08, 2008.
[9]
D. Clément, T. Despeyroux, G. Kahn, and J. Despeyroux. A Simple Applicative Language: mini-ML. In LFP'86, 1986.
[10]
W. R. Cook. A denotational semantics of inheritance. PhD thesis, Providence, RI, USA, 1989. AAI9002214.
[11]
T. Coquand and Gérard Huet. The calculus of constructions. Technical Report RR-0530, INRIA, May 1986.
[12]
N. A. Danielsson. Operational semantics using the partiality monad. In ICFP'12, 2012.
[13]
B. Delaware, W. R. Cook, and D. Batory. Product lines of theorems. In OOPSLA'11, 2011.
[14]
L. Duponcheel. Using catamorphisms, subtypes and monad transformers for writing modular functional interpreters., 1995.
[15]
J. Gibbons and R. Hinze. Just do it: simple monadic equational reasoning. In ICFP'11, 2011.
[16]
J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1), Jan. 1977.
[17]
G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer. How to make ad hoc proof automation less ad hoc. In ICFP'11, 2011.
[18]
R. Hinze. Church numerals, twice! JFP, 15(1):1--13, 2005.
[19]
G. Hutton. A tutorial on the universality and expressiveness of fold. J. Funct. Program., 9(4):355--372, 1999.
[20]
M. Jaskelioff, N. Ghani, and G. Hutton. Modularity and implementation of mathematical operational semantics. Electron. Notes Theor. Comput. Sci., 229(5), March 2011.
[21]
G. Lee, B. C. d. S. Oliveira, S. Cho, and K. Yi. Gmeta: A generic formal metatheory framework for first-order representations. In ESOP 2012, 2012.
[22]
X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7), 2009.
[23]
M. Y. Levin and B. C. Pierce. Tinkertype: A language for playing with formal systems. Journal of Functional Programming, 13(2), March 2003.
[24]
S. Liang and P. Hudak. Modular denotational semantics for compiler construction. In ESOP'96, 1996.
[25]
S. Liang, P. Hudak, and M. Jones. Monad transformers and modular interpreters. In POPL'95, 1995.
[26]
D. MacQueen. Modules for standard ML. In LFP'84, 1984.
[27]
G. Malcolm. Algebraic Data Types and Program Transformation. PhD thesis, Rijksuniversiteit Groningen, September 1990.
[28]
E. Moggi. Notions of computation and monads. Inf. Comput., 93(1), July 1991.
[29]
A. Mulhern. Proof weaving. In WMM '06, September 2006.
[30]
B. C. d. S. Oliveira. Modular visitor components. In ECOOP'09, 2009.
[31]
B. C. d. S. Oliveira and W. R. Cook. Extensibility for the masses: Practical extensibility with object algebras. In ECOOP'12, 2012.
[32]
B. C. d. S. Oliveira, R. Hinze, and A. Löh. Extensible and modular generics for the masses. In Trends in Functional Programming, 2006.
[33]
B. C. d. S. Oliveira, T. Schrijvers, and W. R. Cook. Effectiveadvice: disciplined advice with explicit effects. In AOSD'10, 2010.
[34]
C. Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In TLCA'93, 1993.
[35]
F. Pfenning and C. Paulin-Mohring. Inductively defined types in the calculus of constructions. In MFPS V, 1990.
[36]
F. Pfenning and C. Schürmann. System description: Twelf - a metalogical framework for deductive systems. In CADE'99, 1999.
[37]
B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
[38]
A. M. Pitts. Nominal logic, a first order theory of names and binding. Inf. Comput., 186(2):165--193, 2003.
[39]
Robert Pollack. How to believe a machine-checked proof. In Twenty Five Years of Constructive Type Theory, 1998.
[40]
Christopher Schwaab and Jeremy G. Siek. Modular type-safety proofs using dependant types. CoRR, abs/1208.0535, 2012.
[41]
Peter Sewell et al. Ott: effective tool support for the working semanticist. In ICFP'07, 2007.
[42]
M. Sozeau and N. Oury. First-class type classes. In TPHOLs '08, 2008.
[43]
W. Swierstra. Data types `a la carte. J. Funct. Program., 18(4), 2008.
[44]
T. Uustalu and V. Vene. Coding recursion a la Mendler. In WGP'00, pages 69--85, 2000.
[45]
P. Wadler. The Expression Problem. Email, November 1998. Discussion on the Java Genericity mailing list.
[46]
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad hoc. In POPL'89, pages 60--76, 1989.

Cited By

View all
  • (2025)Progressful Interpreters for Efficient WebAssembly MechanisationProceedings of the ACM on Programming Languages10.1145/37048589:POPL(627-655)Online publication date: 9-Jan-2025
  • (2023)A Type-Based Approach to Divide-and-Conquer Recursion in CoqProceedings of the ACM on Programming Languages10.1145/35711967:POPL(61-90)Online publication date: 11-Jan-2023
  • (2019)Completeness Theorems for First-Order Logic Analysed in Constructive Type TheoryLogical Foundations of Computer Science10.1007/978-3-030-36755-8_4(47-74)Online publication date: 20-Dec-2019
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. coq
  2. extensible church encodings
  3. modular mechanized meta-theory

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)40
  • Downloads (Last 6 weeks)9
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Progressful Interpreters for Efficient WebAssembly MechanisationProceedings of the ACM on Programming Languages10.1145/37048589:POPL(627-655)Online publication date: 9-Jan-2025
  • (2023)A Type-Based Approach to Divide-and-Conquer Recursion in CoqProceedings of the ACM on Programming Languages10.1145/35711967:POPL(61-90)Online publication date: 11-Jan-2023
  • (2019)Completeness Theorems for First-Order Logic Analysed in Constructive Type TheoryLogical Foundations of Computer Science10.1007/978-3-030-36755-8_4(47-74)Online publication date: 20-Dec-2019
  • (2018)Efficient Mendler-Style Lambda-Encodings in CedilleInteractive Theorem Proving10.1007/978-3-319-94821-8_14(235-252)Online publication date: 4-Jul-2018
  • (2016)The Design and Formalization of Mezzo, a Permission-Based Programming LanguageACM Transactions on Programming Languages and Systems10.1145/283702238:4(1-94)Online publication date: 2-Aug-2016
  • (2014)Type Soundness and Race Freedom for MezzoFunctional and Logic Programming10.1007/978-3-319-07151-0_16(253-269)Online publication date: 2014
  • (2024)The Linguistics of ProgrammingProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3689492.3689806(162-182)Online publication date: 17-Oct-2024
  • (2024)Abstract Interpreters: A Monadic Approach to Modular VerificationProceedings of the ACM on Programming Languages10.1145/36746468:ICFP(602-629)Online publication date: 15-Aug-2024
  • (2024)Deriving Dependently-Typed OOP from First PrinciplesProceedings of the ACM on Programming Languages10.1145/36498468:OOPSLA1(983-1009)Online publication date: 29-Apr-2024
  • (2024)Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational EffectsProceedings of the ACM on Programming Languages10.1145/36498218:OOPSLA1(276-304)Online publication date: 29-Apr-2024
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media