| 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
|
