Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs

DOI10.1007/978-3-030-00389-0_3OpenAlexW2890321676MaRDI QIDQ1798782

Stefano Berardi, Makoto Tatsuta

Publication date: 23 October 2018

Full work available at URL: https://hal.inria.fr/hal-02044649/file/473364_1_En_3_Chapter.pdf

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items (2)

Polarized subtyping ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An intuitionistic version of Ramsey's theorem and its use in program termination
• Games for the \(\mu\)-calculus
• Results on the propositional \(\mu\)-calculus
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Cyclic Arithmetic Is Equivalent to Peano Arithmetic
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Sequent calculi for induction and infinite descent
• Cyclic proofs of program termination in separation logic
• Automated Cyclic Entailment Proofs in Separation Logic
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs