Guarded Dependent Type Theory with Coinductive Types

DOI10.1007/978-3-662-49630-5_2zbMath1475.68060arXiv1601.01586OpenAlexW2964301529MaRDI QIDQ2811330

Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Type theory (03B38)

Related Items

When programs have to watch paint dry, Lewis meets Brouwer: constructive strict implication, Streams of approximations, equivalence of recursive effectful programs, Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda, A model of guarded recursion via generalised equilogical spaces, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Denotational semantics of recursive types in synthetic guarded domain theory, A Light Modality for Recursion, Denotational semantics for guarded dependent type theory, Adjoint reactive GUI programming, Temporal refinements for guarded recursive types, Coinduction in Flow: The Later Modality in Fibrations, Unnamed Item, Guarded Dependent Type Theory with Coinductive Types, Modal dependent type theory and dependent right adjoints, Guarded cubical type theory

Uses Software

• Coq
• Nuprl
• Irdis
• Idris
• cubicaltt

Cites Work

• Categorical logic and type theory
• Guarded Dependent Type Theory with Coinductive Types
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A very modal model of a modern, major, general type system
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• A type theory for productive coprogramming via guarded recursion
• Wellfounded recursion with copatterns
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects
• A model of guarded recursion with clock synchronisation
• A model of PCF in guarded type theory