RDP
MEETINGS
VENUE

TLCA'03

6th International Conference on Typed Lambda Calculi and Applications
Valencia, Spain, June 1012, 2003

ABSTRACTS OF INVITED TALKS
A Logical Algorithm for ML Type Inference

David McAllester
(Toyota Technological Institute at Chicago, USA)

This paper gives a bottomup logic programming formulation of the HindleyMilne
r polymorphic type inference algorithm.
We show that for programs of bounded order and arity the given algorithm runs i
n O(n \alpha(n) + d n) time where n is the length of the program,
d is the "scheme depth" of the program, and \alpha is the inverse of
Ackermann's function.
It is argued that for practical programs d will not exceed 5 even for
programs with hundreds of module layers.
This formulation of the HindleyMilner algorithm is intended as a case study in
"logical algorithms", i.e., algorithms
presented and analyzed as bottomup inference rules.

Higher order beta matching

Ralph Loader

We show that solving higher order matching problems up to
beta equivalence, is not decidable. We illustrate the proof
technique on 4th order unification, and then fill in the gaps to
reach higher order matching.

Formalizing the proof of the fourcolortheorem

Georges Gonthier
(l'École Polytechnique  INRIA Rocquencourt, Le Chesnay Cedex, France)

Last update Apr 2003 # sescobar@dsic.upv.es
