Using Structural Recursion for Corecursion

DOI10.1007/978-3-642-02444-3_14zbMath1246.68196MaRDI 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 theory; Coq; structural recursion; coinductive types; guarded corecursion

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

Related Items

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