Constructive Type Classes in Isabelle
From MaRDI portal
Publication:3612442
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
Related Items
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
