Generating linear orders for datatypes

MaRDI QIDQ7361531FDO

Authors René Thiemann

Publication date 7 August 2012

Cites work

• Certification of Termination Proofs Using CeTA
• Light-weight containers for Isabelle: efficient, extensible, nestable
• The Isabelle collections framework

Cited in

(5)

• Strong Eventual Consistency of the Collaborative Editing Framework WOOT
• A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
• Verified Complete Test Strategies for Finite State Machines
• Haskell's Show Class in Isabelle/HOL
• An Algebra for Higher-Order Terms

This page was built for software: Generating linear orders for datatypes