|Number of watchers on Github||40|
|Number of open issues||0|
|Open pull requests||0+|
|Closed pull requests||0+|
|Last commit||almost 4 years ago|
|Repo Created||almost 4 years ago|
|Repo Last Updated||about 2 years ago|
|Organization / Author||scmu|
|Do you use foundations-harper? Leave a review!|
|View foundations-harper activity|
|View on github|
|Fresh, new opensource launches 🚀🚀🚀|
Trendy new open source projects in your inbox! View examples
Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages. Languages from the followings chapters of the book are defined:
For each language, we basically define its typing rules, its small step semantics, and prove the subject reduction (preservation) and progress theorems.
The proofs represents terms in Arthur Charguraud's locally nameless style with cofinite quantification, with my own little variation: terms are indexed by number of bound variables. Terms are thus always locally closed. I found this made some proofs much easier.