This project contains a partial formalization of Pure Type Systems (PTS), written in Agda.
The code makes heavy use of the Agda standard library, which is freely available here. It has been tested using Agda 2.5.3 and version 0.14 of the Agda standard library.
For an excellent introduction to pure type systems, see H. P. Barendregt's Lambda Calculi with Types, chapter 2 of the Handbook of Logic in Computer Science (vol. 2), Oxford University Press, 1992.
Copyright (c) 2015 EPFL