[Prev][Next][Index][Thread]

MIT TOC Seminar--Jerzy Tiuryn--Tue. Oct. 10, 1989

Date: Thu, 5 Oct 89 10:25:37 EDT
To: theory-seminars@theory.LCS.MIT.EDU

                Massachusetts Institute of Technology
                    Theory of Computation Seminar

                   DATE: Tuesday, October 10, 1989
                         REFRESHMENTS: 4:00pm
                             TALK: 4:15pm
                           PLACE: NE43-512A

  "Polymorphic Type Reconstruction in ML-like Programming Languages"

                        Professor Jerzy Tiuryn
              University of Warsaw and Boston University
                            Warsaw, Poland

We survey our recent solutions to several problems in the area of type
reconstruction problems for ML, its extensions, and various fragments
of the second-order lambda-calculus:

-- the ML-typability problem is DEXPTIME-complete (settling an open
   problem of Kanellakis and Mitchell).

-- typability in ML+``polymorphic recursion'' is undecidable.

-- typability, in any fixed rank greater than 2, of the second-order
   lambda-calculus with constants is undecidable.

-- typability in rank 2 second-order lambda-calculus is
   polynomial-time equivalent to the ML-typability (with or without
   constants).

The undecidability results follow from our result that:

-- the semi-unification problem is undecidable (settling an open
   problem in proof theory).

However, the major problem of the type reconstruction problem for the
full second-order lambda-cxalculus still remains open.

These are joint results with A.J. Kfoury, P. Urzyczyn.

HOST: Prof. Albert Meyer