Pointers in Recursion: Exploring the Tropics
From MaRDI portal
Recommendations
Cites work
- A Kripke logical relation between ML and assembly
- A relationally parametric model of dependent type theory
- Canonicity and normalization for dependent type theory
- Categorical logic and type theory
- Categories for Types
- Conservativity of equality reflection over intensional type theory
- Generalized algebraic theories and contextual categories
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 1342278 (Why is no real title available?)
- Internal type theory
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Logical relations for a logical framework
- Normalisation by evaluation for type theory, in type theory
- Proofs for free. Parametricity for dependent types
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Type theory in type theory using quotient inductive types
- Univalence for inverse diagrams and homotopy canonicity
Cited in
(9)- Relative full completeness for bicategorical Cartesian closed structure
- Constructive sheaf models of type theory
- A cubical language for Bishop sets
- Multimodal dependent type theory
- Reduction Free Normalisation for a proof irrelevant type of propositions
- For the metatheory of type theory, internal sconing is enough
- Normalization for multimodal type theory
- Normalization for multimodal type theory
- Second-order generalised algebraic theories: signatures and first-order semantics
This page was built for publication: Pointers in Recursion: Exploring the Tropics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089027)
