Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
type: Item
instance of: scholarly article
title: Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
DOI: 10.1145/3531130.3533359
author: Magnus Baunsgaard Kristensen
author: Rasmus Ejlers Møgelberg
author: Andrea Vezzosi
publication date: 2024-12-06T00:00:00Z
Mathematics Subject Classification ID: 03B38
zbMATH DE Number: 7954857
MaRDI profile type: Publication
cites work: Wellfounded recursion with copatterns
cites work: Non-wellfounded trees in Homotopy Type Theory
cites work: A very modal model of a modern, major, general type system
cites work: Productive coprogramming with guarded recursion
cites work: Q5144643
cites work: A presheaf model of parametric type theory
cites work: Guarded cubical type theory
cites work: First steps in synthetic guarded domain theory: step-indexing in the topos of trees
cites work: Guarded Dependent Type Theory with Coinductive Types
cites work: Denotational semantics for guarded dependent type theory
cites work: General Recursion via Coinductive Types
cites work: Internal Parametricity for Cubical Type Theory
cites work: Quotienting the delay monad by weak bisimilarity
cites work: Fitch-style modal lambda calculi
cites work: Programming and Reasoning with Guarded Recursion for Coinductive Types
cites work: Modal dependent type theory and dependent right adjoints
cites work: Cubical Type Theory: a constructive interpretation of the univalence axiom
cites work: On Higher Inductive Types in Cubical Type Theory
cites work: Q5089011
cites work: Constructive sheaf models of type theory
cites work: Internal type theory
cites work: Multimodal Dependent Type Theory
cites work: Canonicity for cubical type theory
cites work: Iris from the ground up: A modular foundation for higher-order concurrent separation logic
cites work: Q4993352
cites work: Q5141620
cites work: Q3688389
cites work: Applicative programming with effects
cites work: A type theory for productive coprogramming via guarded recursion
cites work: Denotational semantics of recursive types in synthetic guarded domain theory
cites work: Q4611379
cites work: A model of PCF in guarded type theory
cites work: Type-Based Productivity of Stream Definitions in the Calculus of Constructions
cites work: Higher inductive types as homotopy-initial algebras
cites work: Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor.
cites work: Q5089035
cites work: Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
cites work: Cubical Agda: A dependently typed programming language with univalence and higher inductive types
cites work: On the final sequence of a finitary set functor
description: scientific article; zbMATH DE number 7954857