scientific article; zbMATH DE number 7407783
From MaRDI portal
Publication:5155672
zbMath1498.03030arXiv2011.15021MaRDI QIDQ5155672
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
Publication date: 8 October 2021
Full work available at URL: https://arxiv.org/abs/2011.15021
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Finitary type theories with and without contexts ⋮ When programs have to watch paint dry ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ A general framework for the semantics of type theory ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Treatise on intuitionistic type theory
- On the unity of logic
- Notions of computation and monads
- Generalized algebraic theories and contextual categories
- Sheaves in geometry and logic: a first introduction to topos theory
- On an intuitionistic modal logic
- Fitch-style modal lambda calculi
- An algorithm for type-checking dependent types
- Canonicity and normalization for dependent type theory
- A judgmental reconstruction of modal logic
- Categorical Homotopy Theory
- On Irrelevance and Algorithmic Equality in Predicative Type Theory
- Programming and Reasoning with Guarded Recursion for Coinductive Types
- Natural models of homotopy type theory
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- A Contextual Logical Framework
- Polarised subtyping for sized types
- Logic Programming with Focusing Proofs in Linear Logic
- A type theory for productive coprogramming via guarded recursion
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Internal type theory
- Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
- Pointers in Recursion: Exploring the Tropics
- A Generalized Modality for Recursion
- Degrees of Relatedness
- Modalities in homotopy type theory
- Productive coprogramming with guarded recursion
- Contextual modal type theory
- Adjoint Logic with a 2-Category of Modes
- Normalisation by Evaluation for Dependent Types.
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Applicative programming with effects
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories
- Univalence for inverse diagrams and homotopy canonicity
- A presheaf model of parametric type theory
- A model of guarded recursion with clock synchronisation
