Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Practical Type Inference for first-class Polymorphism
Dimitrios Vytiniotis
University of Pennsylvania
SWS Colloquium
Dimitrios Vytiniotis is a PhD candidate in Programming Languages at
the University of Pennsylvania, and is working under the supervision
of Stephanie Weirich. His research interests include programming
languages theory and implementation, type system design, semantics of
programming languages, automated theorem proving, and formal
methods. Dimitrios holds an Electrical Engineering diploma from
National Technical University of Athens, Greece, and has worked as a
software engineer before arriving at Penn.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 7 April 2008
15:00
60 Minutes
E1 5
Rotunda
Saarbrücken
Abstract
Type inference is a key component of modern, statically typed,
functional programming languages, such as Caml and Haskell. It allows
programmers to omit many excessive---and in some cases all---type
annotations from programs.
A different key component of modern programming languages is
polymorphism. However, languages with polymorphism typically have
ad-hoc restrictions on where and what kind of polymorphic types may
occur. Supporting ``first-class'' polymorphism, by lifting those
restrictions, is obviously desirable, but it is hard to achieve
without sacrificing type inference.
In this talk I will explain the difficulties with type inference for
first-class polymorphism, give a historic roadmap of the research
on this topic, and present a new type system for first-class
polymorphism that improves on earlier proposals: it is an extension of
ML type inference; it has a simple, declarative specification;
typeability is robust to program transformations; and the specification
enjoys a sound, complete and decidable type inference algorithm.
This is joint work with Stephanie Weirich and Simon Peyton Jones.
functional programming languages, such as Caml and Haskell. It allows
programmers to omit many excessive---and in some cases all---type
annotations from programs.
A different key component of modern programming languages is
polymorphism. However, languages with polymorphism typically have
ad-hoc restrictions on where and what kind of polymorphic types may
occur. Supporting ``first-class'' polymorphism, by lifting those
restrictions, is obviously desirable, but it is hard to achieve
without sacrificing type inference.
In this talk I will explain the difficulties with type inference for
first-class polymorphism, give a historic roadmap of the research
on this topic, and present a new type system for first-class
polymorphism that improves on earlier proposals: it is an extension of
ML type inference; it has a simple, declarative specification;
typeability is robust to program transformations; and the specification
enjoys a sound, complete and decidable type inference algorithm.
This is joint work with Stephanie Weirich and Simon Peyton Jones.
Contact
Claudia Richter
9325 688
--email hidden
passcode not visible
logged in users only
Uwe Brahm, 04/07/2008 14:54
Claudia Richter, 04/04/2008 09:18 -- Created document.
Claudia Richter, 04/04/2008 09:18 -- Created document.