[Agda] mechanizations of normalization proofs of a list of type theories

[Jason Hu]

Hi all,

as my PhD finally approaches to the end, I have put together the mechanizations in Agda that I have done during my study, where I focus on normalization proofs of different type theories: https://hustmphrrr.github.io/mech-type-theories/

A list of type theories are available here: https://hustmphrrr.github.io/mech-type-theories/README.html

The library contains many type theories, including STLC, MLTT and also my own work. In this library, I implemented different normalization proofs, including presheaf models and untyped domain models based on Andreas' habilitation thesis. It is quite notable that the NbE proof in this library is very concise; it has only 8k LoC and can be shrunk a bit further. I think this is quite amazing, as usually we don't really think that Agda can compress LoC that much compared to, e.g. Coq, proof assistants that come with powerful proof automations. I think the concision of the library not only provides research value, but also should be helpful for educational purposes. I also believe this library provides an alternative to other mechanizations out there for people to base their work on. So please do not hesitate and take a quick look!

Since it is very unlikely for me to work on type theory substantially after graduation, at least not full-time, I will probably only spend the minimal effort to make sure that the library catches up with the latest Agda and stdlib. I would like to welcome people to contribute and/or use this library for anything.

Any other suggestions are also welcomed. I will try to address as much as possible before the winter comes.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20240725/522b339c/attachment.html>