Canonicity and normalization for dependent type theory

DOI10.1016/j.tcs.2019.01.015zbMath1454.03019arXiv1810.09367OpenAlexW2963765784WikidataQ128559732 ScholiaQ128559732MaRDI QIDQ2422026

Thierry Coquand

Publication date: 18 June 2019

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1810.09367

zbMATH Keywords

higher-order abstract syntaxdependent type theorynormalisation proof

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (7)

Reduction Free Normalisation for a proof irrelevant type of propositions ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Pointers in Recursion: Exploring the Tropics ⋮ Unnamed Item

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inaccessible set axioms may have little consistency strength
• On Irrelevance and Algorithmic Equality in Predicative Type Theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• The Expressiveness of Simple and Second-Order Type Structures
• Internal type theory
• Parametricity and dependent types
• Normalisation by Evaluation for Dependent Types.
• Intensional interpretations of functionals of finite type I
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: Canonicity and normalization for dependent type theory