Skip to Main content Skip to Navigation
Habilitation à diriger des recherches

Peter, the Language that does not Exist...

Luigi Liquori 1, 2
1 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : It is my privilege and pleasure to introduce Peter, the language that does not exist...
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.). In my opinion, the habilitation thesis should not be a mere translation of the candidate’s most successful papers (3), nor a commented curriculum vitæ, nor a survey of all the related works in his scientific area (4), just to mention a few “classic Habilitation styles”. It is my opinion that it should be short in length since it is experienced that a very few Habilitation thesis are really downloaded, cited and read. Oftenly, habilitation thesis are not even made accessible on the Web.
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, Benjamin and Phil’s Featherweight Java [IPW01] and Alonso Church’s typed lambda calculus [Chu41]. 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 (see item (Type-programmable)). 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 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 (6), 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 in 2004 [Bra04] 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, and inspired by the works of Kim [Bru99, TKB01, BDKT03, RBC+ 05, Bru02] and Gilles [Dow03, Dow07], I wish you a very nice reading of the Peter’s Habilitation.
3 Although certain parts are taken of my articles.
4 The typographic convention is that references to my papers are in “numeric” style while references to other papers are in “alphanumeric” style.
6 We provide a CD and a Web site with all my papers.
Document type :
Habilitation à diriger des recherches
Complete list of metadatas

Cited literature [112 references]  Display  Hide  Download
Contributor : Luigi Liquori <>
Submitted on : Monday, May 4, 2015 - 5:07:41 PM
Last modification on : Wednesday, October 14, 2020 - 4:24:16 AM
Long-term archiving on: : Wednesday, April 19, 2017 - 3:12:26 PM


  • HAL Id : tel-01148503, version 1



Luigi Liquori. Peter, the Language that does not Exist.... Computation and Language [cs.CL]. INPL - INP de LORRAINE, 2007. ⟨tel-01148503⟩



Record views


Files downloads