Programming and Reasoning with Guarded Recursion for Coinductive Types
From MaRDI portal
Publication:2949454
DOI10.1007/978-3-662-46678-0_26zbMath1459.68034arXiv1501.02925OpenAlexW2963638222MaRDI QIDQ2949454
Hans Bugge Grathwohl, Ranald Clouston, Aleš Bizjak, Lars Birkedal
Publication date: 1 October 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1501.02925
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)
Related Items
Normalization by evaluation for modal dependent type theory, Lewis meets Brouwer: constructive strict implication, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, A model of guarded recursion with clock synchronisation, A model of PCF in guarded type theory, A Light Modality for Recursion, Unnamed Item, Guarded Dependent Type Theory with Coinductive Types, Modal dependent type theory and dependent right adjoints, Unnamed Item
