pl-semantics-and-types

Rocq Development overview

• common
  • common.core Autosubst core definitions
  • common.fintype Autosubst fin type
  • common.fin_util Additional properties of fin type
  • common.renaming Language independent lemmas about renamings
  • common.relations Multistep reduction
• STLC: Simply Typed Lambda Calculus
  • syntax.sig Autosubst input
  • stlc.syntax Definition of the syntax (generated)
  • stlc.typing Typing relation
  • stlc.red Small-step and big-step operational semantic
  • stlc.safety Preservation and progress
  • stlc.small_step Properties of small-step and multistep evaluation
  • stlc.red_equiv Equivalence between small-step and big-step
  • stlc.soundness Termination (totality) of big-step semantics
• REC: Fine-grained CBV with recursive values and recursive types
  • syntax.sig Autosubst input for terms
  • rec.syntax Generate term syntax
  • rec.typesyntax Autosubst input for REC types
  • rec.typesyntax Generated type syntax
  • rec.reduction Small-step operational semantics. Includes some notes about Autosubst and various properties of the small-step relation.
  • rec.typing Typing relation, preservation and progress proofs
  • rec.extensions Derived syntactic forms for fine-grained CBV
  • rec.semsound Cannot show termination for multistep evaluation (incomplete proof)
  • rec.iprop propositions indexed by steps
  • rec.stepsLR Definition of step-indexed logical relation via strong induction (requires proof irrelevance)
  • rec.steps Proof of semantic soundness for step-indexed logical relation
  • rec.stepsAlt Proof of semantic soundness for step-indexed logical relation, uses structural induction only, and no proof irrelevance
  • rec.prim Primitive reductions in a separate judgement.
  • rec.stack Operational semantics with an explicit stack.
• DIV: type-and-effect system for nontermination
  • div.eff Effect annotations (a pre-ordered monoid)
  • div.typesyntax.sig Syntax of REC types with latent effects
  • div.typesyntax Syntax of REC types with latent effects (generated)
  • div.div Type soundness and Effect soundness
• MODAL: monadic type system for nontermination
  • modal.syntax
  • modal.modal Call-by-value language with monadic encapsulation of nontermination
  • modal.modal_intrinsic Interpretation of annotated version of the modal type system in type theory (i.e. Rocq’s Gallina language). Requires an intrinistically-typed version of the syntax.
• CONTROL: exceptions, continuations, and effect handlers
  • control.syntax.sig
  • control.syntax Syntax of a language with exceptions, continuations and effect handlers
  • control.typesyntax.sig
  • control.typesyntax
  • control.control Type system, operational semantics and soundness proofs
  • control.letcc Language with continuations only
  • control.cps Continuation-Passing-Style translation for letcc language
  • control.callcc Classical logic examples
• UNTYPED: untyped lambda calculus and program equivalence
  • untyped.syntax.sig
  • untyped.syntax.v
  • untyped.prim.v Primitive reductions
  • untyped.stack.v Stack-based operational semantics
  • untyped.ctx.v CTX relation as largest adequate compatible pre-order
  • untyped.equiv.v CTX is equivalent to CIU (via step-indexed logical relation)
  • untyped.contextual.v CTX is equivalent to Contextual equivalence
  • untyped.example_equiv.v Examples
  • rec.simple_equiv.v Equivalence for simply-typed language

This site is open source. Improve this page.