scientific article; zbMATH DE number 7649963
From MaRDI portal
Publication:5875422
Recommendations
- Programming and reasoning with guarded recursion for coinductive types
- Guarded dependent type theory with coinductive types
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Formalized, effective domain theory in Coq
- Circular coinduction in Coq using bisimulation-up-to techniques
- Inductive and coinductive components of corecursive functions in Coq
- CoCaml: functional programming with regular coinductive types
- Initial semantics for higher-order typed syntax in \textsf{Coq}
- Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
- Towards Rewriting in Coq
Cites work
- scientific article; zbMATH DE number 949290 (Why is no real title available?)
- scientific article; zbMATH DE number 7199590 (Why is no real title available?)
- scientific article; zbMATH DE number 7649963 (Why is no real title available?)
- A lattice-theoretical fixpoint theorem and its applications
- An introduction to (co)algebra and (co)induction
- Hammer for Coq: automation for dependent type theory
- Inductive types and type constraints in the second-order lambda calculus
- Introduction to bisimulation and coinduction
- Practical coinduction
- The power of parameterization in coinductive proof
- Universal coalgebra: A theory of systems
- Well-founded recursion with copatterns and sized types
Cited in
(2)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875422)
