hdm-fully-grounding

Formalization of a fully grounding type inference algorithm for the HDM system

Building

Dependencies

This mechanisation has been tested with Coq versions 8.16.0 and 8.16.1. It depends on Penn's Metalib library. Pull and follow instructions from https://github.com/plclub/metalib .

Building the project

The _Coqproject has been included in the repository. It should not be necessary to touch this, but it can be regenerated by calling ./configure in the coq subdirectory.

Call make in the coq subfolder. Alternatively, to build in parallel, call make -j n where n is the amount of threads on your machine

Description of files

• coq:
  • Complete: definitions and theorems proving completeness
  • Cpdtlib: library, http://adam.chlipala.net/cpdt/ , exports crush
  • Defs: definitions and theorems about the system, not specific to either soundness or completeness
  • Libtactics: library, https://softwarefoundations.cis.upenn.edu/plf-current/LibTactics.html , exports inverts, splits, gen etc. Excerpt from https://www.chargueraud.org/softs/tlc/ . Note that this mechanisation does not depend on the axioms declared.
  • Prelude: A set of imports and tactics every file imports
  • Sound: definitions and theorems proving soundness
  • Wf: definitions and theorems proving the well-formedness of various elements under various transformations
  • Wf: definitions and theorems proving the well-formedness of various elements under various transformations
  • scripts: script for generating `_Coqproject'
  • z_VerifyAssumptions.v: checks assumptions for soundness and completeness theorems
• delta.pdf: description of the delta between the paper and the mechanisation
• Ott:
  • Hdm.pdf: Latex Ott export
  • Hdm.tex: file to compile to obtain Hdm.pdf
  • HdmDefs.ott: Specification of system in Ott dsl
  • HdmDefs.tex: raw Ott .tex output, imported by Hdm.tex