Type Assigment Systems for Lambda Calculi and for the Lambda Calculus of Objects
Systèmes d'inférence de type pour le lambda-calcul et pour le lambda-calcul à objets
Sistemi di Assegnamento di tipi per il lambda calcolo e per il lambda calcolo degli oggetti
Résumé
This thesis is part of the study of Type Theory for the λ-calculus. It is divided into a "foundational" part and in an "applicative" part:
i) The foundational part studies various type assignment systems for the untyped λ-calculus. In particular the main properties of such systems were proved and were considered the relations with the corresponding type systems for the typed λ-calculus and with intuitionistic logic.
ii) The applicative part studies a possible extension of the λ-calculus to a language that can be seen as a "paradigm" to study new programming techniques such as object-oriented programming. A type assignment system for such language has been defined and the fundamental properties of the system were proved.
Cette thèse fait partie de l'étude de la théorie des types pour le λ-calcul. Il est divisé en une partie "fondamentale" et une partie "applicative":
i) La partie fondamentales étudie différents systèmes d ínference de type pour le λ-calcul non typé. En particulier, les principales propriétés de ces systèmes ont été prouvées comme e.g. les relations avec les systèmes de type correspondantes pour le λ-calcul typé et avec la logique intuitionniste.
ii) La partie applicative étudie une extension possible du λ-calcul à un langage qui peut être considéré comme un «paradigme» pour étudier de nouvelles techniques de programmation tels que la programmation orientée objet. Un système d'inférence de type pour un tel langage a été défini et les propriétés fondamentales du système ont été demontrés.
Questa tesi si inserisce nell’ambito dello studio della Teoria dei Tipi per il λ-calcolo. É suddivisa in una parte “fondazionale” ed in una “applicativa”:
i) La parte fondazionale studia vari sistemi di assegnazione di tipi per il λ-calcolo puro. In particolare sono state provate le proprietà fondamentali di tali sistemi e sono stati considerati i rapporti con i corrispondenti sistemi di tipi per il λ-calcolo tipato e con la logica intuizionista.
ii) La parte applicativa studia una possibile estensione del λ-calcolo ad un linguaggio che può essere visto come “paradigma” per studiare tecniche nuove di programmazione come l’Object Oriented. Un sistema di assegnazione di tipi per tale linguaggio è stato definito e le proprietà fondamentali di tale sistema sono state provate.