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

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