Foundational extensible corecursion: a proof assistant perspective
From MaRDI portal
Publication:2981955
DOI10.1145/2784731.2784732zbMath1360.68358arXiv1501.05425OpenAlexW2147890340MaRDI QIDQ2981955
Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette
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
Related Items (13)
Soundness and completeness proofs by coinductive methods ⋮ Formalization of the resolution calculus for first-order logic ⋮ A Consistent Foundation for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Friends with Benefits ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ A consistent foundation for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Compositional Coinduction with Sized Types ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Model Finding for Recursive Functions in SMT
Uses Software
This page was built for publication: Foundational extensible corecursion: a proof assistant perspective
