Modular Termination Verification: Machine-Checked Proofs

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