Witnessing (co)datatypes

DOI10.1007/978-3-662-46669-8_15MaRDI QIDQ2802441zbMATHOpenAlexFDO

Authors Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01212587/file/wit.pdf

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Truly modular (co)datatypes for Isabelle/HOL
• Foundational (co)datatypes and (co)recursion for higher-order logic
• Foundational nonuniform (co)datatypes for higher-order logic
• A decision procedure for (co)datatypes in SMT solvers
• A decision procedure for (co)datatypes in SMT solvers

Cited in

(9)

• Foundational nonuniform (co)datatypes for higher-order logic
• A formalized hierarchy of probabilistic system types. Proof pearl
• Foundational (co)datatypes and (co)recursion for higher-order logic
• Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
• Friends with benefits. Implementing corecursion in foundational proof assistants
• scientific article; zbMATH DE number 7471712 (Why is no real title available?)
• A decision procedure for (co)datatypes in SMT solvers
• Truly modular (co)datatypes for Isabelle/HOL
• A decision procedure for (co)datatypes in SMT solvers

Describes a project that uses

Uses Software

• Isabelle/HOL
• CIRC
• ProofPower
• HOL Light

This page was built for publication: Witnessing (co)datatypes

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