Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2012/13 / Oberseminar / Matthias Benkard, Type Checking Without Types


Matthias Benkard, Type Checking Without Types

TCS Oberseminar 9.11.2012 14:15 Uhr L109
Wann 14:15 15:15 09.11.2012
von bis
Wo L109
Termin übernehmen vCal

Matthias Benkard
Type Checking Without Types

We propose a programming language with a type system roughly based on dependent types, but built on top of mereology rather than set theory (and thus without the need for a Set type). In our formalism, typing is equivalent to subtyping; that is, a value is a member of the type T iff it is a subtype of T.

Since every value is a type, there is no need for special syntax for the declaration or definition of types. In particular, algebraic data types can be defined through the same fixed-point mechanism that is used for recursive function definitions. Similarly, arrow types are functions, employing pattern matching just as their ``members'' do. Finally, Sigma-types can be represented by object comprehensions.


abgelegt unter: