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

parametricityhigher-order logicIsabelleproof assistants(co)recursion

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)

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

Describes a project that uses

Uses Software

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

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)