Formal definitions and proofs for partial (co)recursive functions
From MaRDI portal
Cites work
- A constructive denotational semantics for Kahn networks in Coq
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
- Containers: Constructing strictly positive types
- Domain interpretations of Martin-Löf's partial type theory
- Final Coalgebras are Ideal Completions of Initial Algebras
- Friends with benefits. Implementing corecursion in foundational proof assistants
- General Recursion via Coinductive Types
- Guarded recursion in Agda via sized types
- HOLCF = HOL + LCF
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 107999 (Why is no real title available?)
- scientific article; zbMATH DE number 3469994 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 2003155 (Why is no real title available?)
- scientific article; zbMATH DE number 1424015 (Why is no real title available?)
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Indexed containers
- Inductive and coinductive components of corecursive functions in Coq
- Introduction to bisimulation and coinduction
- Non-wellfounded trees in homotopy type theory
- On coalgebras over algebras
- Partiality and recursion in interactive theorem provers -- an overview
- Representing continuous functions between greatest fixed points of indexed containers
- Terminal coalgebras in well-founded set theory
- The \textsc{MetaCoq} project
- The optimal fixed point combinator
- The Theoretical Aspects of the Optimal Fixedpoint
- Typed Lambda Calculi and Applications
- Universal coalgebra: A theory of systems
This page was built for publication: Formal definitions and proofs for partial (co)recursive functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6615564)
