scientific article; zbMATH DE number 7779294

arXiv2207.00843MaRDI QIDQ6068934

Andreas Nuyts, Dominique Devriese, Unnamed Author

Publication date: 15 December 2023

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A dependent type theory with abstractable names
• The calculus of constructions
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Extending Type Theory with Forcing
• A type theory for synthetic $\infty$-categories
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Internal type theory
• Relational Parametricity for Higher Kinds
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Denotational semantics for guarded dependent type theory
• Degrees of Relatedness
• A Constructive Model of Directed Univalence in Bicubical Sets
• Modal dependent type theory and dependent right adjoints
• Adjoint Logic with a 2-Category of Modes
• Category Theory in Coq 8.5
• Interactive proofs in higher-order concurrent separation logic
• A relationally parametric model of dependent type theory
• Theorem Proving in Higher Order Logics
• Internal Parametricity for Cubical Type Theory
• Unifying Cubical Models of Univalent Type Theory
• A presheaf model of parametric type theory

This page was built for publication: