Rocoma.Autosubst.AutosubstSsr

• Autosubst wrapper for ssreflect

Rocoma.Lib.Autosubst_FreeVars

• Free variables for Autosubst terms
  • Single-variable substitutions
  • Definition of non-free variables and related lemmas.

Rocoma.Lib.My_tactics

• Tactics

Rocoma.Coma

• Coma expressions (TOPLAS section 2)
  • Syntax, TOPLAS Fig. 2
  • Typing, TOPLAS Fig. 3
  • Semantics, TOPLAS Fig. 4

Rocoma.Extraction

• Extraction of the evaluator to OCaml

Rocoma.Main

• Summary: assumptions and proofs
  • Assumed
  • Definitions used in the statements
  • Proved, TOPLAS section 3 and appendix D
  • Axioms used

Rocoma.Recipes

• Recipes: syntax, substitutions, neutralization, weight and depth
  • AST
  • Decidability lemmas
  • Type classes instanciations
  • Key Definitions
  • Basic lemmas related to these key definitions

Rocoma.Recipes_box_rel

• The box condition

Rocoma.Recipes_directly_box

• Directly boxed subrecipes

Rocoma.Recipes_eval

• Evaluation of complete recipes (TOPLAS Theorem 3.2)

Rocoma.Recipes_evalf

• A functional evaluator

Rocoma.Recipes_fusion

• Fusion and meet (TOPLAS 3.7 to 3.10)
  • Fusion (TOPLAS page 13)

Rocoma.Recipes_fv_lemmas

• Free variables of recipes
  • Renamings and substitutions under upn

Rocoma.Recipes_joker

• Jokers (TOPLAS Theorem 3.11)
  • The joker, TOPLAS Fig. 6
  • Closed in both sorts
  • Neutralization: z becomes Top
  • Typing
  • Covers and submits
  • Evaluation of the joker
  • Calls of the items
  • D.1 and 3.11

Rocoma.Recipes_logrel

• Logical relations (TOPLAS Lemma 3.1)

Rocoma.Recipes_neuneu

• Neutrality and entailment (TOPLAS 3.3 to 3.6)
  • Zeros under boxes
  • Neutrality
  • Entailment

Rocoma.Recipes_stacks

• Stacks and application chains
  • Stacks

Rocoma.Recipes_typing

• Typing of recipes, with forbidden windows
  • Typing judgment
  • Renaming and substitution of handlers

Rocoma.Recipes_valid_model

• A model of the validity axioms
  • Definitions
  • Auxiliary lemmas
  • The rules of VALID

Rocoma.Recipes_valid_sig

• Signature of the validity relation

Rocoma.VCgen

• Verification condition generation (TOPLAS section 4)
  • TOPLAS 3.11 shortcuts
  • VC generation, TOPLAS Fig. 9
  • Typing
  • Substitutions
  • TOPLAS Lemma F.1
  • Closing substitutions
  • UNIFORM
  • Uniform neutrality
  • TOPLAS Lemma 4.1 (F.2)
  • Uniform equivalence
  • TOPLAS Lemma F.3
  • TOPLAS Lemma F.4
  • TOPLAS Lemma 4.2 (F.5)