Witnessing (co)datatypes

DOI10.1007/978-3-662-46669-8_15MaRDI QIDQ2802441zbMATH OpenOpenAlexFDO

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

(10)

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

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)