Agda, Finally...

WIP

I'm not sure what to write here...

While I cannot ensure all the accompanied texts or explanation are correct, at least all the Agda code type checks :D

References

Here are the major references for this repo:

• Programming Language Foundations in Agda
• Programming Language Foundations
• An Introduction to Logical Relations
• Type safety in STLC using logical relation
• Autosubst: Automation for de Bruijn syntax and substitution in Coq
• Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions
• Explicit substitutions
• A concrete framework for environment machines
• POPLMark reloaded: Mechanizing proofs by logical relations
• System F in Agda, for Fun and Profit