micro Agda TySy
The purpose of this project is to formalize a basic functional language with its type system and to prove the well known safety theorem.
The project is divided in multiple files:
basic.agdacontains common basic definitions.list.agdacontains all about lists, both functions that deals with lists and proofs of useful propositions.nat.agdacontains all about natural numbers.type-system.agdais the main file. It contains the language formalization and all the steps that brings to the proof of the safety theorem.examples.agdacontains examples of type judgments or evaluation judgments.
I suggest to start the reading from type-system.agda and then to switch to other files as needed.
The latex compiler used is xelatex.