Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Principal Typings for Explicit Substitutions Calculi

Author(s): Daniel Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine
Slot: Array, 16:30-16:50, col. 5


Having principal typings (for short PT) is an important property of type
systems. In simply typed systems, this property guarantees the possibility of a
complete and terminating type inference mechanism. It is well-known that the
simply typed lambda-calculus has this property but recently  J.B. Wells has
introduced a system-independent definition of PT, which allows to prove that
some type systems, e.g. the Hindley/Milner type system, do not satisfy PT.
Explicit substitutions address a major computational drawback of the
lambda-calculus and allow the explicit treatment of the substitution operation
to formally correspond to its implementation. Several extensions of the
lambda-calculus with explicit substitution  have been given  but some of which
do not preserve basic properties such as the preservation of strong
normalization. We consider two systems of explicit substitutions (lambda s_e and
lambda sigma) and show that they can be accommodated with an adequate notion of
PT. Specifically, our results are as follows:

  - We introduce PT  notions for the simply typed versions of the lambda s_e-
and the lambda-sigma-calculi and  prove that they agree with Wells' notion
of PT.

  - We show that these versions satisfy PT by revisiting previously
  introduced type inference algorithms.

websites: Arnold Beckmann 2008-05-18