Foundational (co)datatypes and (co)recursion for higher-order logic

DOI10.1007/978-3-319-66167-4_1zbMath1495.68238OpenAlexW2746677766MaRDI QIDQ1687535

Ondřej Kunčar, Jasmin Christian Blanchette, René Thiemann, Christian Sternagel, Martin Desharnais, Fabian Meier, Julian Biendarra, Andreas Lochbihler, Mathias Fleury, Johannes Hölzl, Lorenz Panny, Andrei Popescu, Dmitriy Traytel, Aymeric Bouzy

Publication date: 4 January 2018

Full work available at URL: https://hal.inria.fr/hal-01592196/file/BiendarraBlanchetteEtAl-FroCos.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

Unnamed Item ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ A case study in programming coinductive proofs: Howe’s method

Uses Software

• Coq
• Nitpick
• Isabelle/HOL
• Isar
• z3
• Kodkod
• Coinductive
• Jinja Threads
• Markov Models
• Knuth Bendix Orders
• Abstract Completeness
• Deriving class
• Nested Multisets

This page was built for publication: Foundational (co)datatypes and (co)recursion for higher-order logic