Campus Event Calendar
Event Entry
What and Who
Towards a flexible type system with subtypes and parametric polymorphism for constraint logic programming
Francois Fages
CNRS, Ecole Normale Superieure, Paris
Logik-Seminar
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 22 April 97
16:15
60 Minutes
46.1 - MPII
019
Saarbrücken
Abstract
The static type system of Mycroft-O'Keefe and Reddy, adapted from
ML to logic programs, fails to type meta-programming predicates,
or constraint logic programs over a structure X, which is often
a combination of basic structures: integers, reals, lists, terms,
feature structures, etc. The introduction of a subtyping relation
solves these problems, but raises several difficulties for detecting
type errors statically. There are several approaches to these
difficulties. We present a type system for CLP(X) languages, in
which types are partially ordered first-order terms, called poterms.
The problem of statically checking program types reduces to solving
a left-linear system of inequations between poterms that is shown
to be easily decidable with existence of a most general solution.
Then we discuss type inference for predicates, with the notion
of most informative type, defined as the most general type w.r.t.
variable instantiation and the most specific w.r.t. subtyping.
ML to logic programs, fails to type meta-programming predicates,
or constraint logic programs over a structure X, which is often
a combination of basic structures: integers, reals, lists, terms,
feature structures, etc. The introduction of a subtyping relation
solves these problems, but raises several difficulties for detecting
type errors statically. There are several approaches to these
difficulties. We present a type system for CLP(X) languages, in
which types are partially ordered first-order terms, called poterms.
The problem of statically checking program types reduces to solving
a left-linear system of inequations between poterms that is shown
to be easily decidable with existence of a most general solution.
Then we discuss type inference for predicates, with the notion
of most informative type, defined as the most general type w.r.t.
variable instantiation and the most specific w.r.t. subtyping.
Contact
Uwe Waldmann
(0681) 9325-227, uni-intern: 92227
--email hidden
passcode not visible
logged in users only