NDLI: Static and user-extensible proof checking

Content Provider	ACM Digital Library
Author	Shao, Zhong Stampoulis, Antonis
Abstract	Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely time-consuming. We argue that this can be attributed to two profound shortcomings in the architecture of modern proof assistants. The first is that proofs need to include a large amount of minute detail; this is due to the rigidity of the proof checking process, which cannot be extended with domain-specific knowledge. In order to avoid these details, we rely on developing and using tactics, specialized procedures that produce proofs. Unfortunately, tactics are both hard to write and hard to use, revealing the second shortcoming of modern proof assistants. This is because there is no static knowledge about their expected use and behavior. As has recently been demonstrated, languages that allow type-safe manipulation of proofs, like Beluga, Delphin and VeriML, can be used to partly mitigate this second issue, by assigning rich types to tactics. Still, the architectural issues remain. In this paper, we build on this existing work, and demonstrate two novel ideas: an extensible conversion rule and support for static proof scripts. Together, these ideas enable us to support both user-extensible proof checking, and sophisticated static checking of tactics, leading to a new point in the design space of future proof assistants. Both ideas are based on the interplay between a light-weight staging construct and the rich type information available.
Starting Page	273
Ending Page	284
Page Count	12
File Format	PDF MP4
ISSN	03621340 15581160
DOI	10.1145/2103621.2103690
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	47
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	Type theory Tactic development Conversion rule Dependent types Proof assistants
Content Type	Audio 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

Static and user-extensible proof checking

Parametric higher-order abstract syntax for mechanized semantics

VeriML:typed computation of logical terms inside a language with effects

Effective interactive proofs for higher-order imperative programs

Dijkstra monads for free

Canonicity for 2-dimensional type theory

Modular development of certified program verifiers with a proof assistant

Dependent types and multi-monadic effects in F*

Hybrid type checking

Static and user-extensible proof checking

Similar Documents

Static and user-extensible proof checking

Parametric higher-order abstract syntax for mechanized semantics

VeriML:typed computation of logical terms inside a language with effects

Effective interactive proofs for higher-order imperative programs

Dijkstra monads for free

Canonicity for 2-dimensional type theory

Modular development of certified program verifiers with a proof assistant

Dependent types and multi-monadic effects in F*

Hybrid type checking

Static and user-extensible proof checking