TY - GEN

T1 - Principal typings for explicit substitutions calculi

AU - Ventura, Daniel Lima

AU - Ayala-Rincón, Mauricio

AU - Kamareddine, Fairouz

PY - 2008

Y1 - 2008

N2 - 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 ?-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 ?-calculus and allow the explicit treatment of the substitution operation to formally correspond to its implementation. Several extensions of the ?-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 (?s e and ?s) 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 ?s e - and the ?s-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. © 2008 Springer-Verlag Berlin Heidelberg.

AB - 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 ?-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 ?-calculus and allow the explicit treatment of the substitution operation to formally correspond to its implementation. Several extensions of the ?-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 (?s e and ?s) 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 ?s e - and the ?s-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. © 2008 Springer-Verlag Berlin Heidelberg.

KW - Explicit substitution

KW - Lambda-calculus

KW - Principal typings

UR - http://www.scopus.com/inward/record.url?scp=45849118005&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-69407-6_60

DO - 10.1007/978-3-540-69407-6_60

M3 - Conference contribution

SN - 3540694056

SN - 9783540694052

VL - 5028 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 567

EP - 578

BT - Logic and Theory of Algorithms - 4th Conference on Computability in Europe, CiE 2008, Proceedings

T2 - 4th Conference on Computability in Europ

Y2 - 15 June 2008 through 20 June 2008

ER -