Using Structural Recursion for Corecursion

DOI10.1007/978-3-642-02444-3_14MaRDI QIDQ3638255zbMATH OpenOpenAlexFDO

Authors 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

Coqconstructive type theorystructural recursioncoinductive typesguarded corecursion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Structured general corecursion and coinductive graphs (extended abstract)
• Inductive and coinductive components of corecursive functions in Coq
• A term calculus for (co-)recursive definitions on streamlike data structures
• Foundational extensible corecursion: a proof assistant perspective
• Concrete stream calculus: an extended study

Cites work

• scientific article; zbMATH DE number 2185697 (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 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Coinductive field of exact real numbers and general corecursion
• Functional differentiation of computer programs
• Inductive and coinductive components of corecursive functions in Coq
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanizing coinduction and corecursion in higher-order logic
• Productivity of Stream Definitions
• Terminating general recursion
• Type-based termination of recursive definitions
• Typed Lambda Calculi and Applications

Cited in

(10)

• (Co)inductive proof systems for compositional proofs in reachability logic
• Checking equivalence of corecursive streams: an inductive procedure
• Checked corecursive streams: expressivity and completeness
• Structured general corecursion and coinductive graphs (extended abstract)
• Structural recursion with locally scoped names
• The never-ending recursion
• Foundational extensible corecursion: a proof assistant perspective
• Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
• Automatically Introducing Tail Recursion in CakeML
• Friends with benefits. Implementing corecursion in foundational proof assistants

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3638255)