15-317 Constructive Logic
Software

SML

We assume that all students know how run Standard ML of New Jersey, or some other SML compiler.

Prooftree

For much of the course, we will be using an automated proof checker called Prooftree. Prooftree runs on Gradescope, but its interface is an SML library that we provide. You can compile the interface wherever you run SML, which will allow you to check locally that your submission is free of syntax errors.

An auxiliary tool to help you get used to Prooftree is Proof Tree Generator.

Dcheck

Dcheck is an experimental derivation parser and checker. Its documentation is here. An example file is here. Dcheck runs on Gradescope, but you can run its sanity-checking features on Andrew at ~crary/bin/dsanity.

Prolog

In the middle part of the course, we will be writing programs in Prolog. Two good, free Prolog interpreters are GNU-Prolog and SWI-Prolog.

[ Home | Schedule | Assignments | Software ]