Inductive and Coinductive Components of Corecursive Functions in Coq
From MaRDI portal
Publication:2873661
DOI10.1016/j.entcs.2008.05.018zbMath1279.68285MaRDI QIDQ2873661
Ekaterina Komendantskaya, Yves Bertot
Publication date: 24 January 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.05.018
Related Items
Coinductive predicates and final sequences in a fibration, A Type-Theoretic Approach to Resolution, Coinductive predicates and final sequences in a fibration, (Co)inductive proof systems for compositional proofs in reachability logic, Non-well-founded deduction for induction and coinduction, Friends with Benefits, Formal polytypic programs and proofs, Using Structural Recursion for Corecursion, Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The calculus of constructions
- Terminating general recursion
- The temporal semantics of concurrent programs
- A term calculus for (co-)recursive definitions on streamlike data structures
- Affine functions and series with co-inductive real numbers
- Mechanizing coinduction and corecursion in higher-order logic
- Type-based termination of recursive definitions
- Foundations of Software Science and Computation Structures
- General Recursion via Coinductive Types
- Productivity of Stream Definitions
- Modelling general recursion in type theory
- Typed Lambda Calculi and Applications