scientific article; zbMATH DE number 7288622

MaRDI QIDQ5141620

Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri

Publication date: 18 December 2020

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

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

zbMATH Keywords

denotational semanticsdependent type theoryguarded recursioncoinductive typesmodal types

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (1)

Unnamed Item

Uses Software

• cubicaltt

Cites Work

• A dependent type theory with abstractable names
• Fitch-style modal lambda calculi
• The Guarded Lambda-Calculus: 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
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• Denotational semantics for guarded dependent type theory
• Guarded Computational Type Theory
• Multimodal Dependent Type Theory
• A Model of Countable Nondeterminism in Guarded Type Theory
• Modal dependent type theory and dependent right adjoints
• Wellfounded recursion with copatterns
• Productive coprogramming with guarded recursion
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Applicative programming with effects
• A presheaf model of parametric type theory
• Unnamed Item
• Unnamed Item

This page was built for publication: