Inductive and Coinductive Components of Corecursive Functions in Coq

DOI10.1016/j.entcs.2008.05.018zbMath1279.68285OpenAlexW2074746292MaRDI 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

inductioncoinductionguardednessCoqaccessibility predicatesproductiveness

Mathematics Subject Classification ID

Related Items (9)

Coinductive predicates and final sequences in a fibration ⋮ Friends with Benefits ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ A Type-Theoretic Approach to Resolution ⋮ Formal polytypic programs and proofs ⋮ Non-well-founded deduction for induction and coinduction ⋮ Using Structural Recursion for Corecursion ⋮ Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme ⋮ Coinductive predicates and final sequences in a fibration

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

This page was built for publication: Inductive and Coinductive Components of Corecursive Functions in Coq