SML code for Handbook of Practical Logic and Automated Reasoning - For Isabelle too
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
code
README.md Update README.md Jan 8, 2017

README.md

SML-Handbook - SML version of code for John Harrison's "Handbook of Practical Logic and Automated Reasoning" (Chapter 6 on Interactive Theorem Proving only)

For Isabelle, Moscow ML, Standard ML of New Jersey and Poly/ML.

New entry in the Archive of Formal Proofs: https://www.isa-afp.org/entries/FOL_Harrison.shtml

The verification in Isabelle of the kernel is described here:

Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen: Verification of an LCF-Style First-Order Prover with Equality. Isabelle Workshop 2016: http://www21.in.tum.de/~nipkow/Isabelle2016/

Please provide feedback to Associate Professor Jørgen Villadsen, DTU Compute, Denmark: http://people.compute.dtu.dk/jovi/