This repository houses λProlog translations of various programming languages described in the book Types and Programming Languages (TAPL), by Benjamin Pierce. Select theorems, lemmas, and exercises have been translated into abella proofs.
| Module | Chapter |
|---|---|
| tyarith.mod | Chapter 8 - Typed Arithmetic Expressions |
| simple.mod | Chapter 9 - Simply Typed Lambda Calculus |
| simplebool.mod | Chapter 9 - Simply Typed Lambda Calculus |
| simpleunit.mod | Chapter 11 - Simple Extensions (Section 11.2) |
To install teyjus and abella using opam:
$ opam switch create tapl 4.14.1
$ eval $(opam env --switch=tapl)
$ opam pin add teyjus 'git+https://github.com/teyjus/teyjus#v2.1.1'
$ opam install abella