Home | Search | Help  
Home Page Università di Genova

Seminar Details


Date 17-12-2007
Time 11:00
Room/Location DISI - Aula 218 - 2° piano
Title
Speaker Dott. Luigi Liquori
Affiliation INRIA Sophia Antipolis
Link http://www-sop.inria.fr/mascotte/Luigi.Liquori/HDR/Peter.Pan.html
Abstract Luigi Liquori plays his Habilitation Thesis: "Peter, the language that does not exists..." informal scientific "pièce" in 3 parts: PIECE CAPSULE: The Peter language contains almost the linguistic features I have introduced and investigated in the field of functional and object-oriented programming, plus some new features not published yet. In Peter's Habilitation, I will try to limit as much as possible the mathematical overhead and the technicalities (e.g. full set of rules, full proofs of theorems, etc). Peter's Habilitation will be based on the following three points: [Modularity] I will present a (Turing complete) kernel of Peter, called Baby Peter, and I will continue in the rest of the Habilitation to extend it in a modular fashion until the final extension, called Wise Peter. Baby Peter is a functional language with object-oriented features equipped with a sound type system. Peter bears some similarities to Atsushi Igarashi, Benjamin Pierce and Phil Wadler's Featherweight Java and Alonso Church's typed lambda calculus. The main difference lies in an "ad hoc" exception-handling mechanism allowing the programmer to choose the type system according to her/his necessities and goals. Even more, it allows the programmer to write her/his own type system. Some chapters will focus on operational semantics, some others on type systems, some others on both. All topics will be treated in a "lightweight fashion". Examples of extensions are for instance mixing class-based and pure object-based features, but also improving proof languages à la Logical Framework(LF) with pattern matching facilities and including those metalanguages to Peter in order to mix algorithms and their correctness proofs. [Verbatim-like] Instead of annoying the reader with a plain French translation of some of my most relevant papers, I will show, for each extension, only some key rules of the operational semantics or of the type system (every system has at least a key rule...) and some motivating examples. I do not plan to prove type soundness for each extension of Peter: the whole soundness of Wise Peter is left as a challenge for the "next" user friendly proof assistant. [Type-programmable] Type systems for programming languages and proof languages are fixed "a priori" by language designers; type systems are not first class citizens. To my little knowledge, no language allows the programmer to build, choose, or mix type systems. The idea of modifying the type discipline at compile time is not completely new; a quite inspiring work has been done by the "visionary-6-pages" paper by Gilad Bracha in 2004 called "Pluggable Type Systems". The possibility to mixing type systems and using it as a first class citizens is an interesting research strand that will constitute an original contribution in Peter's Habilitation. With the intention of disseminating science in a simple, clear and pedagogical way, I wish you a very nice hearing/reading of the Peter's Habilitation. PART ONE: The Young Peter (Learning) - act 1: Peter Learns How to Learn - act 2: Peter Learns with Two Hands PART TWO: Peter, the Man (Expertise) - act 3: Peter Becomes a Specialist - act 4: Peter can Fly PART THREE: Peter, the Old Man (Reasoning) - act 5: Peter and the Nowhere Island - act 6: Peter Becomes Wiser - QUESTIONS THANKS images courtesy by Walt Disney music courtesy by Beatles
Back to Seminars