Witnessing (co)datatypes

DOI10.1007/978-3-662-46669-8_15zbMATH Open1335.68224OpenAlexW2183882274MaRDI QIDQ2802441FDOQ2802441

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

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

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Cited In (9)

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

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)