Using Structural Recursion for Corecursion

DOI10.1007/978-3-642-02444-3_14zbMath1246.68196OpenAlexW1532383456MaRDI QIDQ3638255

Yves Bertot, Ekaterina Komendantskaya

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02444-3_14

zbMATH Keywords

constructive type theoryCoqstructural recursioncoinductive typesguarded corecursion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (4)

Checked corecursive streams: expressivity and completeness ⋮ The never-ending recursion ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme

Uses Software

• Coq
• ML
• Isabelle/HOL
• HOL
• Agda

Cites Work

• 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.
• Terminating general recursion
• Isabelle/HOL. A proof assistant for higher-order logic
• Inductive and Coinductive Components of Corecursive Functions in Coq
• Mechanizing coinduction and corecursion in higher-order logic
• Type-based termination of recursive definitions
• Productivity of Stream Definitions
• Typed Lambda Calculi and Applications
• Functional differentiation of computer programs

This page was built for publication: Using Structural Recursion for Corecursion