Formalising the Eiffel Typesystem
- Supervisor Dr. Joseph Kiniry
- Subject Area Programming Languages
- Pre-requisites Excellent maths ability
- Co-requisites (things you must learn along the way) Very good knowledge of the Eiffel programming language, and good knowledge of type theory, and basic use of PVS
- Subject Coverage Programming Languages, Type Theory, Theorem Provers
- Project Type Theory
- Hardware/Software Machine running anything but Windows
Description
Eiffel is a strongly-typed object-oriented programming language. Eiffel is widely regarded as one of the best OO languages available today. Eiffel was created in the late 1980s by Bertrand Meyer, who now holds the Chair of Software Engineering at ETHZ.
The Eiffel language definition is found in a book called "Eiffel the Language", originaly published by Prentice-Hall in 1990 (often called ETL for short). The language definition consists of a few hundred pages of precise natural language, much like the Java Language Specification (aka, JLS) published by Addison-Wesley and Sun.
In the Java world, a very large amount of research has gone into formalising Java's type system and semantics. Because Eiffel is a much less popular language, correspondingly less research has been done on Eiffel's formal foundations. That work that does exist was done back in the early-to-mid 1990s.
Throughout the past 10 years the Eiffel language has evolved as new language features were experimented with by the developers and users of the main commercial and FLOSS compilers, EiffelStudio and SmartEiffel, respectively.
Eiffel is now being standardised by ECMA. A core set of Eiffel experts are working on the new language definition, incorporating many of the new ideas from various compilers and other new languages. An updated version of ETL is being written now as a result of this work (called ETL3 for historical reasons).
To deeply understand this new Eiffel from a formal point-of-view, the first necessary step is to formalise the new type system. The aim of this project is to define this new type system and investigate its properties.
Mandatory Goals
- Read the both versions of "Eiffel the Language."
- Enumerate, classify, and analyse the changes contained in ETL3.
- Review the existing literature on the formalisation of Eiffel.
- Formalise the ETL3 type system.
Discretionary Goals
- Become familiar with at least one logical framework in which the Eiffel type system will be formalised.
- Encode the ETL3 type system in the chosen framework.
Exceptional Goals
- Analyse the soundness of the ETL3 type system.
- Characterise interesting properties of the ETL3 type system.
- Write, submit, and publish a paper on the results.