Project Page Index Table of Contents
  • Tools for modular syntax with binders
    • Basic definitions
    • MetaCoq Commands
    • Tactics for modular syntax
  • Introductory example: counting funtions
    • manual definitions
    • using our tools
  • Case study 1: Modular Type-Safety Proofs (originally in Agda)
    • Arithmetic expressions
    • Option expressions
    • Array expressions
    • Composed development
  • Case Study 2: Monotonicty and Type Safety for big-step mini-ML
    • Autosubst 2 generated code
    • mini-ML: lambda expression
    • mini-ML: boolean expressions
    • mini-ML: arithmetic expressions
    • mini-ML: natCase expressions
    • mini-ML: recursive abstractions
    • Autosubst 2 generated combined mini-ML types
    • Autosubst 2 generated combined mini-ML types without fix
    • Composed results for mini-ML
    • Composed results for mini-ML witout fix
  • Case study 3: Type preservation, weak head normalisation and strong normalisation for mini-ML
    • Autosubst 2 generated code
    • mini-ML: Variables
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • mini-ML: Lambda expressions
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • MiniML: Boolean expressions
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • mini-ML: Arithmetic terms
      • Preservation
      • Weak Head Normalisation
      • Strong Normalisation
    • Composition
      • Definition of typing
      • Definition of evaluation
      • Type preservation
      • Weak Normalisation
      • Strong Normalisation
Generated by coqdoc and improved with CoqdocJS