Pointers in Recursion: Exploring the Tropics

DOI10.4230/LIPIcs.FSCD.2019.25OpenAlexW2902687082MaRDI QIDQ5089027

Ambrus Kaposi, Simon Huber, Christian Sattler

Publication date: 18 July 2022

Full work available at URL: https://hal.archives-ouvertes.fr/hal-01934791

zbMATH Keywords

Martin-Löf type theorylogical relationsparametricitycanonicityquotient inductive types

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Related Items (4)

Constructive sheaf models of type theory ⋮ Reduction Free Normalisation for a proof irrelevant type of propositions ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Canonicity and normalization for dependent type theory
• Type theory in type theory using quotient inductive types
• Proofs for free
• Logical relations for a logical framework
• Categories for Types
• Internal type theory
• Conservativity of equality reflection over intensional type theory
• A relationally parametric model of dependent type theory
• A kripke logical relation between ML and assembly
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: Pointers in Recursion: Exploring the Tropics