This repository contains the implementation and proofs contained within Benjamin Pierce's book, Types and Programming Languages.
While the code provided with the book is in Ocaml, this repository reproduces the book code in Athena. Further, this repository includes proofs (also in Athena) of the lemmas and theorems that are proven informally within the text.