Organizing numerical theories using axiomatic type classes
type: Item
instance of: scholarly article
title: Organizing numerical theories using axiomatic type classes
zbMATH Open document ID: 1071.68092
published in: Journal of Automated Reasoning
publication date: 2005-05-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 2168288
zbMATH Keywords: arithmetic
zbMATH Keywords: axiomatic type classes
zbMATH Keywords: Isabelle
zbMATH Keywords: overloading
zbMATH Keywords: polymorphism
author: Lawrence C. Paulson
describes a project that uses: ML
describes a project that uses: IMPS
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
MaRDI profile type: Publication
full work available at URL: s10817-004-3997-6
OpenAlex ID: W1997142472
Wikidata QID: Q57382667
cites work: IMPS: An interactive mathematical proof system
cites work: Mechanizing Nonstandard Real Analysis
cites work: A constructive algebraic hierarchy in Coq.
cites work: Q5287513
cites work: Verified bytecode verifiers.
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q5687569
DBLP publication ID: journals/jar/Paulson04
DOI: 10.1007/S10817-004-3997-6
Recommended article: New Computational Paradigms
Recommended article: Arithmetic and the theory of types
Recommended article: Q3478383
Recommended article: Type theory and formalisation of mathematics
Recommended article: Q4204148
Recommended article: Formalising Mathematics in Simple Type Theory
Recommended article: Type classes for mathematics in type theory
Recommended article: Working with Mathematical Structures in Type Theory
Recommended article: Q4247306
Recommended article: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
description: scientific article; zbMATH DE number 2168288