Constructive Type Classes in Isabelle

DOI10.1007/978-3-540-74464-1_11zbMath1178.68529OpenAlexW2146104088MaRDI QIDQ3612442

Florian Haftmann, Makarius Wenzel

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (29)

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Automating change of representation for proofs in discrete mathematics (extended version) ⋮ A modular first formalisation of combinatorial design theory ⋮ Validating Mathematical Structures ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL ⋮ A verified ODE solver and the Lorenz attractor ⋮ CoSMed: a confidentiality-verified social media platform ⋮ A Consistent Foundation for Isabelle/HOL ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Programming and automating mathematics in the Tarski-Kleene hierarchy ⋮ Combining higher-order logic with set theory formalizations ⋮ Exploring the structure of an algebra text with locales ⋮ Unnamed Item ⋮ Formal power series ⋮ From types to sets by local type definition in higher-order logic ⋮ The Isabelle Framework ⋮ First-Class Type Classes ⋮ A consistent foundation for Isabelle/HOL ⋮ Linear quantifier elimination ⋮ From LCF to Isabelle/HOL ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Local Theory Specifications in Isabelle/Isar ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Locales: a module system for mathematical theories ⋮ Formalizing complex plane geometry

Uses Software

• Isabelle
• Isabelle/Isar

This page was built for publication: Constructive Type Classes in Isabelle