General Recursion via Coinductive Types
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 2003149
- Simple general recursion in type theory
- scientific article; zbMATH DE number 1863381
- Typing total recursive functions in Coq
- Modelling general recursion in type theory
- scientific article; zbMATH DE number 883893
- A coinductive completeness proof for the equivalence of recursive types
- scientific article; zbMATH DE number 1424015
- scientific article; zbMATH DE number 2185708
- scientific article; zbMATH DE number 1183236
Cited in
(53)- Terminating general recursion
- General recursive functions in a very simply interpretable typed -calculus
- Typing total recursive functions in Coq
- Complete Elgot monads and coalgebraic resumptions
- Monads for behaviour
- scientific article; zbMATH DE number 1670732 (Why is no real title available?)
- Another look at function domains
- Inductive, coinductive, and pointed types
- The coinductive resumption monad
- Inductive and coinductive components of corecursive functions in Coq
- Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
- Turing-Completeness Totally Free
- Global semantic typing for inductive and coinductive computing
- Unifying guarded and unguarded iteration
- Partiality, Revisited
- Generalizing inference systems by coaxioms
- Partiality, state and dependent types
- A coinductive calculus for asynchronous side-effecting processes
- Implementing Cantor's paradise
- Some Domain Theory and Denotational Semantics in Coq
- Trace-Based Coinductive Operational Semantics for While
- Galois Connections for Recursive Types
- A Type of Partial Recursive Functions
- Computation by Prophecy
- A coinductive calculus for asynchronous side-effecting processes
- scientific article; zbMATH DE number 1497869 (Why is no real title available?)
- Quotienting the delay monad by weak bisimilarity
- Denotational semantics of recursive types in synthetic guarded domain theory
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- scientific article; zbMATH DE number 1424015 (Why is no real title available?)
- scientific article; zbMATH DE number 7080198 (Why is no real title available?)
- Soundness conditions for big-step semantics
- The Scott model of PCF in univalent type theory
- Partiality and Container Monads
- Semantic subtyping for non-strict languages
- Representing continuous functions between greatest fixed points of indexed containers
- Terminal semantics for codata types in intensional Martin-Löf type theory
- Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot
- Logical Approaches to Computational Barriers
- A model of PCF in guarded type theory
- Streams of approximations, equivalence of recursive effectful programs
- Coalgebras in functional programming and type theory
- Formal definitions and proofs for partial (co)recursive functions
- Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
- Two guarded recursive powerdomains for applicative simulation
- Inductive and coinductive predicate liftings for effectful programs
- Representing guardedness in call-by-value and guarded parametrized monads
- What monads can and cannot do with a bit of extra time
- What monads can and cannot do with a few extra pages
- Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
- Comodule representations of second-order functionals
- Primitive recursive dependent type theory
- Uniform Elgot iteration in foundations
This page was built for publication: General Recursion via Coinductive Types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5310638)
