Deriving Comparators and Show Functions in Isabelle/HOL

DOI10.1007/978-3-319-22102-1_28zbMath1465.68063OpenAlexW2407034734MaRDI QIDQ2945654

René Thiemann, Christian Sternagel

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_28

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Certifying proofs in the first-order theory of rewriting

Uses Software

• Isabelle
• Isabelle/HOL
• Haskell
• HOL
• CeTA

Cites Work

• Partial and nested recursive function definitions in higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Truly Modular (Co)datatypes for Isabelle/HOL
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Certification of Termination Proofs Using CeTA
• Code Generation via Higher-Order Rewrite Systems
• Applications of Polytypism in Theorem Proving
• Derivable Type Classes
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• The Isabelle Collections Framework

This page was built for publication: Deriving Comparators and Show Functions in Isabelle/HOL