[FOM] VeriML

[Guillaume Fortaine]

Hello,

For your information :

http://www.cs.yale.edu/homes/stampoulis/

"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."

Best Regards,

Guillaume FORTAINE