Inductive and coinductive components of corecursive functions in Coq
From MaRDI portal
Recommendations
- Structured general corecursion and coinductive graphs (extended abstract)
- scientific article; zbMATH DE number 2003155
- General Recursion via Coinductive Types
- Foundational extensible corecursion: a proof assistant perspective
- Type-Based Productivity of Stream Definitions in the Calculus of Constructions
Cites work
- A term calculus for (co-)recursive definitions on streamlike data structures
- Affine functions and series with co-inductive real numbers
- Coinductive field of exact real numbers and general corecursion
- Foundations of Software Science and Computation Structures
- General Recursion via Coinductive Types
- scientific article; zbMATH DE number 1670732 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 1223736 (Why is no real title available?)
- scientific article; zbMATH DE number 1231567 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 1064116 (Why is no real title available?)
- scientific article; zbMATH DE number 2003149 (Why is no real title available?)
- scientific article; zbMATH DE number 2003155 (Why is no real title available?)
- scientific article; zbMATH DE number 2087341 (Why is no real title available?)
- scientific article; zbMATH DE number 2087345 (Why is no real title available?)
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- scientific article; zbMATH DE number 1424015 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Mechanizing coinduction and corecursion in higher-order logic
- Modelling general recursion in type theory
- Productivity of Stream Definitions
- Proof-assistants using dependent type systems
- Simple general recursion in type theory
- Terminating general recursion
- The calculus of constructions
- The temporal semantics of concurrent programs
- Type-based termination of recursive definitions
- Typed Lambda Calculi and Applications
Cited in
(21)- Nested abstract syntax in Coq
- (Co)inductive proof systems for compositional proofs in reachability logic
- Non-well-founded deduction for induction and coinduction
- Coinductive predicates and final sequences in a fibration
- From Sets to Bits in Coq
- Foundational extensible corecursion: a proof assistant perspective
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Formal polytypic programs and proofs
- Extraction in Coq: An Overview
- Subset Coercions in Coq
- Using Structural Recursion for Corecursion
- Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
- scientific article; zbMATH DE number 2000441 (Why is no real title available?)
- scientific article; zbMATH DE number 2003155 (Why is no real title available?)
- Coinductive predicates and final sequences in a fibration
- A type-theoretic approach to resolution
- Implicit complexity for coinductive data: a characterization of corecurrence
- Structured general corecursion and coinductive graphs (extended abstract)
- scientific article; zbMATH DE number 7649963 (Why is no real title available?)
- Formal definitions and proofs for partial (co)recursive functions
- A general constructive form of Higman's lemma
This page was built for publication: Inductive and coinductive components of corecursive functions in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2873661)
