Inductive and Coinductive Components of Corecursive Functions in Coq

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

zbMATH Keywords

induction; coinduction; guardedness; Coq; accessibility predicates; productiveness

Mathematics Subject Classification ID

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, Friends with Benefits, Formal polytypic programs and proofs, Using Structural Recursion for Corecursion, Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme

Uses Software

• Coq
• Automath

Cites Work

• 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
• 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