Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

26

TPHOL
1997
IEEE

favoriteEmaildiscussreport

107views Automated Reasoning» more TPHOL 1997»

Type Classes and Overloading in Higher-Order Logic

14 years 3 months ago

Type Classes and Overloading in Higher-Order Logic

Download www4.in.tum.de

Type classes and overloading are shown to be independent concepts that can both be added to simple higher-order logics in the tradition of Church and Gordon, without demanding more logical expressiveness. In particular, model-theoretic issues are not aﬀected. Our metalogical results may serve as a foundation of systems like Isabelle/Pure that oﬀer the user Haskell-style order-sorted polymorphism as an extended syntactic feature. The latter can be used to describe simple abstract theories with a single carrier type and a ﬁxed signature of operations.

Markus Wenzel

Real-time Traffic

Automated Reasoning | Extended Syntactic Feature | Simple Abstract Theories | Single Carrier Type | TPHOL 1997 |

claim paper

Related Content

» Typed HigherOrder Narrowing without HigherOrder Strategies

» Functional Programming with Overloading and HigherOrder Polymorphism

» HOLCF Higher Order Logic of Computable Functions

» ObjectOriented Verification Based on Record Subtyping in HigherOrder Logic

» A Typed HigherOrder Calculus for Querying XML Databases

» A Mechanized Translation from HigherOrder Logic to Set Theory

» Code Generation via HigherOrder Rewrite Systems

» Higher Order Quotients and their Implementation in Isabelle HOL

» Functional logic overloading

Post Info
More Details (n/a)

Added	06 Aug 2010
Updated	06 Aug 2010
Type	Conference
Year	1997
Where	TPHOL
Authors	Markus Wenzel

Comments (0)