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

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 machinecheckable proof objects. Unfortunately, large scale proof development in these proof assistants is still an extremely difficult and timeconsuming 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 firstclass 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 ...

• Type: Conference
• Year: 2010
• Where: ICFP
• Authors: Antonis Stampoulis, Zhong Shao
• Keywords: Computational Language, Decision Procedures, ICFP 2010, Programming Languages, Proof Assistants