Program translations of CCω into itself
This repository contains the code carried with the article "The Next 700 Syntactical Models of Type Theory" (CPP 2017).
The directory [Coq formalization](Coq formalization) contains the formalization, in Coq, of sections 3 to 5. See [Coq formalization/Readme.md](Coq formalization/Readme.md).
The directory [Coq plugins](Coq plugins) contains the instrumentation of those sections as Coq plugins. See [Coq plugins/Readme.md](Coq plugins/Readme.md).