Big-step strong call-by-need semantics and efficient convertibility

Coq development

Introduction

The complete sources for this development can be downloaded from the Git repository.

Table of contents

Useful libraries:

• Misc: extended standard library.
• Inductive: auto-generated by an OCaml file, a library for user-defined stronger induction principles.
• GenInd: a library for automatically generating induction principles for nested or mutually-recursive inductive predicates.
• Freevar: free variables and fresh name generation; provides tactics to generate fresh names.
• FEnv: environments, represented as associative lists from free variables to terms.
• Rewrite: general-purpose theorems and definitions for rewriting systems, including the various reflexive, symmetric or transitive closures of relations.
• Costar: coinductive transitive closure of a relation, specifying transitive closure or divergence.
• Pretty: general definitions for pretty-big-step semantics.

The main development:

• STerm: definition of terms, represented by de Bruijn indices, and of substitutions and renamings.
• Beta: definition of beta-reduction and theorems on it, including confluence.
• Red: definition of pretty-big-step substitution semantics.
• RedProof: proof that this semantics is compatible with beta-reduction.
• RedE: definition of pretty-big-step environment semantics.
• RedEProof: proof that this semantics is compatible with the previous one.
• RedM: definition of pretty-big-step call-by-need semantics.
• RedMProof: proof that this semantics is compatible with the previous one.
• Convert: definition of the efficient convertibility machine and its correctness.