RDP                     
Home page
Organization
Sponsors

MEETINGS        
RTA
TLCA
FTP
WG1.6
RULE
UNIF
WFLP
WRS
WST

VENUE               
Valencia
Registration
Accomodation
Travelling
Program
Conference Venue
Internet
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