[Agda] Agda Proofs for Harper's Practical Foundations of Programming Languages

[Shin-Cheng Mu]

Hi all,

I think this might be useful for some of you, so I am 
posting here.

In this repository:

  https://github.com/scmu/foundations-harper

are Agda proofs for some of the theorems in Robert Harper's 
Practical Foundations of Programming Languages (1st edition.. I
haven't got time to update them to the 2nd edition). Languages 
from the followings chapters of the book are defined:

* Ch 4. Statics: L{num str}.
* Ch 8. Function Definitions and Values: L{num str fun}.
* Ch 9. Gödel's T.
* Ch 10. Plotkin’s PCF
* Ch 20. Girard’s System F.

For each language, I basically define its typing rules, its 
small step semantics, and prove the subject reduction 
(preservation) and progress theorems.

The proofs represents terms in Arthur Charguéraud'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 easier.

sincerely,
Shin
scm at iis.sinica.edu.tw