Language Design, Semantics, Types

p> Proposals:

Soundness of the Java Type System Java was designed to support safe, distributed programming on the intrernet. However, several studies point out flaws in its security, and point out the need for a clear understanding of the type system. In this project we will provide a formal semantics and a proof of the soundness of the type system (ie that in a type correct program at run run-time all variables would contain values of the type predicted by the compiler).
Is the C++ type system really safe? The aim of the project is to produce a formal proof of the soundness of the type system; ie that in a type correct program at run run-time all variables would contain values of the type predicted by the compiler. This is an important and non-trivial claim to make: for example, the type system of Eiffel, a highly successful and relatively simple oo programming language, has been discovered not to be sound, a couple of years after the development of the language.
Type Systems for Object Oriented Languages

Java is a simple OO language, developed by SUN to support distributed program development and composition on the Internet. More on Java at our local mirror site.
The possibilities opened by Java are currently being explored. Possible Java applications for student projects could be the animation of algorithms, or interactive packages teaching Maths, or even Java, a simulation package. More sophisticated applications could be Java programming tools, and libraries.

Units and Dimensions for Programming Languages: The type system of a programming language is extended to express dimensions (eg distance, speed), and units for measuring these dimensions (eg km, cm, sec, hr), implicit conversions between units, and operators from units in some dimension to other units in other dimensions. The project requires some innovation, and it involves work in programming language definition and compiler writing.

Higher order Module Parameterization an extension to an existing programming language with modules (eg Modula-2), to allow for parameterization of modules (eg generic lists, and generic matrices expressed in terms of generic lists), and thus a higher level of code reuse. Abstract Datatypes as Afterthoughts A special purpose editor that will assist the improvement of a program to include abstract data types.

Program Beautifier A pre-processor, which would suggest improvements to beginners' programs. It should start with simple improvemenents, as eg replacing if boolexpr1 then if boolexpr2 then ... by if booolexpr1 and boolexpr2 then ... . The make more substantial suggestions which concern data flow and flow of control. If successful, this will be a very useful tool for our students.

Program Beautifier for Smalltalk Similar ideas as above, this time applied to Smalltalk. The advantage of this approach is, that the compiler is part of the environment, and therefore we have direct access to all information required.

Predicates and Quantifiers without Tears - a graphic interactive tool to explain and demonstrate first order predicate calculus.

Smalltalk Program Designer: aims to close the gap between the very high level, language independent design methodologies (like OOA/OOD, OMT etc), and the existing Smalltalk browsers which only support entering programs that are fully designed and thought out.

Arithmetic Tutor - an interactive teacher for basic arithmetic, which sets questions (eg 3*5=?, 6-4=?) according to the pupil's abilities. In addition, when the pupil gives a wrong answer, it supports the pupil, by asking appropriate further questions (eg 3*5=5+5+5=?) to help him/her find the correct answer

Programming Tutor: an interactive system to support teaching of basic programming. The Tutor should consists of a series of lessons. Lessons should consist of short explanatory material together with little tests or little programming assignments which would be tested by the Tutor.