/stlc

This aims to be the most pretentious implementation of stlc in existence

Primary LanguageAgda

Categorical glueing for simply typed lambda calculus

This formalisation mostly follows the 1995 paper Categorical reconstruction of a reduction free normalization proof by Altenkirch at al.

Reading Order

Part I : Objective Metatheory

Defining the Structures

  1. lists: Defines the basic data patterns that we see in contextual categories (𝐢𝑑π‘₯, π‘‡π‘šπ‘ , and π‘‰π‘Žπ‘Ÿ)
  2. contextual: Gives the organising definition behind this implementation; everything is this project relies on contextual structures
  3. ccc: Defines what it means for a contextual category to be cartesian closed, and gives consequences of the structure
  4. functor: Defines contextual functors, constructs composition, and says what it means for a CF to preserve CCC structures

Construstions

  1. psh: Defines a contextual cartesian closed category of presheaves
  2. normal: Defines normal an neutral terms, and related presheaves
  3. twgl: Defines a contextual category of glueings. Shows that any glueing gives rise to a normal form and equality proof
  4. twglccc: Establishes the contextual cartesian closedness of glueings
  5. norm: Establishes that any initial syntactic category has normalisation

Part II : Syntax

  1. syn: Defines the syntactic contextual category
  2. eliminator: Establishes the initiality of syntax
  3. tests: Some applications of our results