Sciweavers

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

12

TPHOL
2008
IEEE

favoriteEmaildiscussreport

126views Automated Reasoning» more TPHOL 2008»

First-Class Type Classes

13 years 10 months ago

First-Class Type Classes

Download mattam.org

Abstract. Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specith abstract structures by quantiﬁcation on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is ﬁrst-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and integrates well inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.

Matthieu Sozeau, Nicolas Oury

Real-time Traffic

Artificial Intelligence | Dependent Type Theory | Specith Abstract Structures | TPHOL 2008 | Type Classes |

claim paper

Related Content

» Type inference for unboxed types and first class mutability

» Type Reconstruction with FirstClass Polymorphic Values

» Type Inference for FirstClass Messages with Feature Constraints

» A Simply Typed Context Calculus with FirstClass Environments

» FirstClass Macros have Types

» Static Dependent Types for First Class Modules

» Subtyping FirstClass Polymorphic Components

» FirstClass Relationships in an ObjectOriented Language

» Information States as First Class Citizens

Post Info
More Details (n/a)

Added	01 Jun 2010
Updated	01 Jun 2010
Type	Conference
Year	2008
Where	TPHOL
Authors	Matthieu Sozeau, Nicolas Oury

Comments (0)