skip to main content
10.1145/2429069.2429094acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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
  • (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
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

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

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (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
  • (2023)Extensible Metatheory Mechanization via Family PolymorphismProceedings of the ACM on Programming Languages10.1145/35912867:PLDI(1608-1632)Online publication date: 6-Jun-2023
  • (2023)Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsProceedings of the ACM on Programming Languages10.1145/35712557:POPL(1801-1831)Online publication date: 11-Jan-2023
  • (2022)LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested DatatypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.360.2360(27-44)Online publication date: 30-Jun-2022
  • (2022)Intrinsically-typed definitional interpreters à la carteProceedings of the ACM on Programming Languages10.1145/35633556:OOPSLA2(1903-1932)Online publication date: 31-Oct-2022
  • (2022)A reasonably gradual type theoryProceedings of the ACM on Programming Languages10.1145/35476556:ICFP(931-959)Online publication date: 31-Aug-2022
  • (2022)Random testing of a higher-order blockchain language (experience report)Proceedings of the ACM on Programming Languages10.1145/35476536:ICFP(886-901)Online publication date: 31-Aug-2022
  • 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