The goal of this project is to define an Embedded Domain Specific Language in Scala to encode and verify deductive systems, such as programming languages and logics. The main inspiration comes from the Twelf system, the most successful implementation of the Edinburgh Logical Framework.
The code includes a Twelf "backend", that can be used to check signatures by using Twelf instead of the more limited typechecking provided in Scala.
This project uses sbt. To compile the code run
sbt compile, and to test run sbt test
To configure the Twelf backend, the binary twelf-server has to be accessible
in the directory of the project. The recommended way to achieve this is by
creating a symbolic link: from the directory containing this file, run the
command ln -s /path/to/twelf-server.