Modular Termination Verification: Machine-Checked Proofs

<p>Machine-checked using Coq 8.6.</p> <p>Contents:</p> <ul> <li><strong>Generic Utility Concepts</strong> <ul> <li><em>Util</em>: Notations for lists and decidable equality</li> </ul> </li> <li><strong>Module Correctness</strong> <ul> <li><em>Programs</em>: The syntax of programs. Parameterized over the set of types, values, and operators, and the well-founded type of levels.</li> <li><em>ProgramExecution</em>: Relates programs to outcomes (termination with a result value or divergence).</li> <li><em>ProgramCorrectness</em>: Correctness of a class, and correctness of a program in terms of correctness of its classes.</li> <li><em>WellTyped</em>: Well-typedness of a program. Implies that the import graph is acyclic.</li> <li><em>Soundness</em>: Correct well-typed programs do not diverge.</li> </ul> </li> <li><strong>Specification Style</strong> <ul> <li><em>NonWf</em>: Relates well-foundedness to descending chains. Used by WellOrderingTheoremEx.</li> <li><em>WellOrderingTheoremEx</em>: Each well-founded relation can be extended to a well-ordering.</li> <li><em>MultisetOrder</em>: Finite multisets, the Dershowitz-Manna ordering, and a proof of its well-foundedness.</li> <li><em>SpecStyle</em>: Instantiates the syntax of programs with a well-founded (in fact: well-ordered) type of method bags.</li> <li><em>MethodBagLemmas</em>: Some lemmas about method bag order, useful for the example correctness proofs.</li> </ul> </li> <li><strong>Example Programs</strong> <ul> <li><em>Loopy</em>: An example program that performs infinite inter-module recursion through dynamic binding.</li> <li><em>PlusOneFunc</em>: An example program with dynamic binding that terminates.</li> <li><em>ExamplesWellTyped</em>: Loopy and PlusOneFunc are well-typed.</li> <li><em>ProgramExecutionTests</em>: Loopy diverges; PlusOneFunc has an execution that terminates with result 0.</li> <li><em>PlusOneFunc_is_Correct</em>: A modular proof of correctness of PlusOneFunc.</li> <li><em>PlusOneFunc_terminates</em>: Applies the soundness theorem to obtain that PlusOneFunc does not have diverging executions.</li> </ul> </li>