Foundational extensible corecursion: a proof assistant perspective

DOI10.1145/2784731.2784732MaRDI QIDQ2981955zbMATH OpenOpenAlexFDO

Authors Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Publication date 10 May 2017

Published in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.05425, https://eprints.mdx.ac.uk/15735/2/ICFP2015.pdf

zbMATH Keywords

(co)recursionhigher-order logicIsabelleparametricityproof assistants

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.

Recommendations

• Friends with benefits. Implementing corecursion in foundational proof assistants
• Inductive and coinductive components of corecursive functions in Coq
• On the Foundations of Corecursion
• Using Structural Recursion for Corecursion
• Mechanizing coinduction and corecursion in higher-order logic

Cited in

(20)

• Formalization of the resolution calculus for first-order logic
• A formalized general theory of syntax with bindings
• A consistent foundation for Isabelle/HOL
• A formalized general theory of syntax with bindings: extended version
• Bisimulation and coinduction enhancements: a historical perspective
• Soundness and completeness proofs by coinductive methods
• Probabilistic functions and cryptographic oracles in higher order logic
• Model finding for recursive functions in SMT
• Inductive and coinductive components of corecursive functions in Coq
• A consistent foundation for Isabelle/HOL
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Comprehending Isabelle/HOL’s Consistency
• On the Foundations of Corecursion
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Using Structural Recursion for Corecursion
• Interactive programming in Agda -- objects and graphical user interfaces
• Proof methods for corecursive programs
• Compositional coinduction with sized types
• A contextual formalization of structural coinduction
• Well-behaved (co)algebraic semantics of regular expressions in Dafny

Describes a project that uses

Uses Software

• Isabelle
• Agda
• Matita
• Coq
• Isabelle/HOL
• PVS

This page was built for publication: Foundational extensible corecursion: a proof assistant perspective

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