NDLI: Engineering formal metatheory

Content Provider	ACM Digital Library
Author	Charguéraud, Arthur Pierce, Benjamin C. Aydemir, Brian Pollack, Randy Weirich, Stephanie
Abstract	Machine-checked proofs of properties of programming languages have become acritical need, both for increased confidence in large and complex designsand as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. There presentation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductivedefinitions of relations on terms (typing, reduction, .). The key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations); in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over other methodologies using first-order representations, leading to developments that are faithful to informal practice, yet require noexternal tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F sub; and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach; they have also been optimized for clarity and robustness, making them good templates for future extension.
Starting Page	3
Ending Page	15
Page Count	13
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/1328897.1328443
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	43
Issue Number	1
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Binding Locally nameless Coq
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Engineering formal metatheory

The Locally Nameless Representation

Verified peephole optimizations for CompCert

Formal verification of SSA-based optimizations for LLVM

A locally nameless solution to the POPLmark challenge

Machine-verified network controllers

Formal design constraints

Product lines of theorems

Verdi: a framework for implementing and formally verifying distributed systems

Engineering formal metatheory

Similar Documents

Engineering formal metatheory

The Locally Nameless Representation

Verified peephole optimizations for CompCert

Formal verification of SSA-based optimizations for LLVM

A locally nameless solution to the POPLmark challenge

Machine-verified network controllers

Formal design constraints

Product lines of theorems

Verdi: a framework for implementing and formally verifying distributed systems

Engineering formal metatheory