Organizing numerical theories using axiomatic type classes

DOI10.1007/s10817-004-3997-6zbMath1071.68092OpenAlexW1997142472WikidataQ57382667 ScholiaQ57382667MaRDI QIDQ1774558

Lawrence Charles Paulson

Publication date: 17 May 2005

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-004-3997-6

zbMATH Keywords

arithmeticpolymorphismIsabelleoverloadingaxiomatic type classes

Mathematics Subject Classification ID

Related Items (5)

Algebraically Closed Fields in Isabelle/HOL ⋮ Formalising Mathematics in Simple Type Theory ⋮ The Isabelle Framework ⋮ Canonical Big Operators ⋮ From LCF to Isabelle/HOL

Uses Software

• ML
• Isabelle/HOL
• HOL
• IMPS

Cites Work

• Unnamed Item
• Unnamed Item
• IMPS: An interactive mathematical proof system
• A constructive algebraic hierarchy in Coq.
• Isabelle/HOL. A proof assistant for higher-order logic
• Verified bytecode verifiers.
• Mechanizing Nonstandard Real Analysis

This page was built for publication: Organizing numerical theories using axiomatic type classes