Keyword: calculus of constructions

• CoqInCoq: A formalisation of the Calculus of Construction
  Bruno Barras
• HistoricalExamples: Historical examples developed in the (pure) Calculus of Constructions
  Christine Paulin, Gérard Huet
• PTS: A formalisation of Pure Type Systems
  Bruno Barras