Library .\Assoc

Library .\ExampleProgram

Library .\ExampleProof

• Validity of the example program's main routine.
• Validity of the incrementor function
• Validity of the dispose function
• Validity of the example module
• Putting it all together: the example program does not get stuck.

Library .\ExampleSpec

Library .\Language

• Syntax
• Semantics
• Some facts about the language

Library .\ProofSystem

• Syntactic assertions
• Function type definitions
• Semantic assertions
• The proof rules

Library .\ProofSystemFacts

Library .\Soundness

• Semantics of closures
• Semantics of function types; meaning of judgments
• Soundness of the proof rules

Library .\Tarski

---

This page has been generated by coqdoc