RDP
MEETINGS
VENUE
|
TLCA'03
|
6th International Conference on Typed Lambda Calculi and Applications
Valencia, Spain, June 10-12, 2003
|
ABSTRACTS OF INVITED TALKS
A Logical Algorithm for ML Type Inference
|
David McAllester
(Toyota Technological Institute at Chicago, USA)
|
This paper gives a bottom-up logic programming formulation of the Hindley-Milne
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 Hindley-Milner algorithm is intended as a case study in
"logical algorithms", i.e., algorithms
presented and analyzed as bottom-up 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 four-color-theorem
|
Georges Gonthier
(l'École Polytechnique - INRIA Rocquencourt, Le Chesnay Cedex, France)
|
Last update Apr 2003 # sescobar@dsic.upv.es
|