A Generalized Modality for Recursion

DOI10.1145/3209108.3209148MaRDI QIDQ5145323zbMATH OpenOpenAlexFDO

Authors Adrien Guatto

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

category theoryfunctional programmingguarded recursionstreamssynchronous programmingtype systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Abstract: Nakano's later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infinite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale. Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.

Recommendations

• General recursion theory. An axiomatic approach
• Modelling general recursion in type theory
• scientific article; zbMATH DE number 2003149
• A general form of relative recursion
• Recursion over realizability structures
• GENERALIZATIONS OF THE RECURSION THEOREM
• Predicate-transformer semantics of general recursion
• Publication:3203736
• scientific article; zbMATH DE number 4091489
• A logic of recursion

Cited in

(14)

• Generic recursive lens combinators and their calculation laws
• Temporal refinements for guarded recursive types
• Time warps, from algebra to algorithms
• Abstract GSOS rules and a modular treatment of recursive definitions
• Dual-context calculi for modal logic
• Guarded computational type theory
• Multimodal dependent type theory
• A model of guarded recursion with clock synchronisation
• Specification and verification of concurrent systems by causality and realizability
• Modal FRP for all: Functional reactive programming without space leaks in Haskell
• Deciding Equations in the Time Warp Algebra
• Totality for mixed inductive and coinductive types
• A calculus for the specification, design, and verification of distributed concurrent systems
• Fan-causality and uniform continuity on final coalgebras

This page was built for publication: A Generalized Modality for Recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145323)