Principal Typings for Explicit Substitutions Calculi

Having principal typings (for short PT) is an important property of type systems. This property guarantees the possibility of type deduction which means it is possible to develop a complete and terminating type inference mechanism. It is well-known that the simply typed -calculus has this property, but recently, J. Wells has introduced a system-independent definition of PT which allows to prove that some type systems do not satisfy PT. The main computational drawback of the -calculus is the implicitness of the notion of substitution, a problem which in the last years gave rise to a number of extensions of the -calculus where the operation of substitution is treated explicitly. Unfortunately, some of these extensions do not necessarily preserve basic properties of the simply typed -calculus such as preservation of strong normalization. We consider two systems of explicit substitutions ( and se) and we show that they can be accommodated with an adequate notion of PT. Specifically, our re...

• Type: Conference
• Year: 2008
• Where: CIE
• Authors: Daniel Lima Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine
• Keywords: Applied Computing, CIE 2008, Satisfy Pt, Short Pt, Type Systems