Paper Info
Title
VeriML: typed computation of logical terms inside a language with effects
Abstract
Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explicit machine-checkable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and time-consuming task. One major weakness of these proof assistants is the lack of a single language where users can develop complex tactics and decision procedures using a rich programming model and in a typeful manner. This limits the scalability of the proof development process, as users avoid developing domain-specific tactics and decision procedures. In this paper, we present VeriML - a novel language design that couples a type-safe effectful computational language with first-class support for manipulating logical terms such as propositions and proofs. The main idea behind our design is to integrate a rich logical framework - similar to the one supported by Coq - inside a computational language inspired by ML. The language design is such that the added features are orthogonal to the rest of the computational language, and also do not require significant additions to the logic language, so soundness is guaranteed. We have built a prototype implementation of VeriML including both its type-checker and an interpreter. We demonstrate the effectiveness of our design by showing a number of type-safe tactics and decision procedures written in VeriML.
Year
DOI
Venue
2010
10.1145/1932681.1863591
international conference on functional programming
Keywords
Field
DocType
large scale proof development,computational language,decision procedure,language design,logical frameworks,type-safe effectful computational language,novel language design,explicit machine-checkable proof object,dependent types,proof assistants,type theory,logic language,logical term,single language,proof assistant,development process,logical framework,higher order logic,programming model
Programming language,Programming paradigm,Computer science,Type theory,Object language,Interpreter,Mathematical proof,Logic programming,Soundness,Logical framework
Conference
Volume
Issue
ISSN
45
9
0362-1340
Citations 
PageRank 
References 
11
0.63
19
Authors
2
Name
Order
Citations
PageRank
Antonis Stampoulis1181.50
Zhong Shao289768.80