README for Veritas
Veritas is a (still very young) prototype for (semi-)automatically proving type soundness using first-order theorem proving as support. It currently allows for specifying the syntax and semantics of very simple programming languages (such as the simply-typed lambda calculus (STLC)), type systems for this language, and proof goals and axioms, via using AST classes. The current version includes a compiler family which allows for translating such language specifications and proof goals on it into TPTP, using different compilation strategies (see "Exploration of Language Specifications by Compilation to First-Order Logic" by Sylvia Grewe, Sebastian Erdweg, Michael Raulf, and Mira Mezini. In: Principles and Practice of Declarative Programming (PPDP). ACM, 2016).
##NOTE: Under construction##
Note that we are currently restructuring Veritas to a stand-alone SBT library which one can use independent of Spoofax, on which the previous version of Veritas heavily relied. Currently, the Veritas project can already be used independent of Spoofax - but using it is not very comfortable (specifying languages by using AST classes, calling Vampire manually on the resulting files etc.). We are currently working on improving the usability of the standalone SBT library.
Meanwhile, the former Spoofax part of Veritas remains functional (with an old Spoofax version, 1.5!) and provides some better usability (see folder VeritasSpoofax for setup instructions).
The old version of Veritas, where the Scala and the Veritas-Spoofax project were still completely integrated with each other is available on the master branch under Tag "PreRestructuing" (including setup instructions). Note that the old version relied on an outdated Spoofax version (1.5).
How to install Veritas (standalone)
- Java 7 or higher
- Installation of SBT and Scala
- (optional) your favorite IDE for Scala
- (optional) your favorite automated theorem prover that understands TPTP, if you would like to prove something, e.g. Vampire (This is currently not required for setting up the Veritas SBT part, but will probably soon be.)
Some optional steps to try with the project:
- Build the project using SBT or your favorite IDE.
- Run "sbt assembly" to produce a standalone .jar of the project (currently not particularly useful in itself, only when using Veritas with VeritasSpoofax).
- Run the tests in test/scala, via your IDE or via "sbt test" (not all of them might work).
- Using for example Scala REPL (or Ammonite, a more advanced REPL), create a language specification using the case classes from the Veritas package, as in some of the tests in test/scala. Your top-level-node should be a "Module". On your Module, you can call transformation steps (see package transformation). For example, you can pass your module to the "MainTrans" object together with a configuration that specifies the compilation strategy. This transformation will apply the necessary basic transformation steps to transform a Veritas module into one or more core modules. On the core module(s), you can apply TypingTrans.finalEncoding to transform the core module into a TPTP file, which you can then pretty-print. See case class EncodingComparison for the first basic steps, and Backend.scala, writeFile for how to pretty-print.