Proofs
Copyright Notice The proofs were based on an existing proof of System-F-Sub in locally nameless by Brian Aydemir and Arthur Charguéraud, Aaron Bohannon, Jeffrey Vaughan, and Dimitrios Vytiniotis. While the definitions heavily changed, the infrastructure code regarding bindings is still very similar.
Proof Sources
The documentation on this page is automatically generated from Coq proof files. The files can be found in the github repository of this artifact:
https://github.com/se-tuebingen/oopsla-2022-artifact/tree/main/coq
Not all proof-files are equally well documented. For the artifact, we carefully prepared the following files, which we recommend to look at.
Definitions of Syntax, Typing, and Semantics
In file Definitions, you can inspect the Coq definitions and compare them with the paper’s definition.
Main Theorems
File Soundness lists the main theorems, like progress and preservation. File Substitution contains lemmas about context weakening as well as the standard substitution lemmas.
Examples
File Examples gives a few worked examples of typed terms and their reductions in System C’s abstract machine model, in particular to show that meaningful terms can be encoded in our Coq formalism of System C.