Practical Research Projects - Project Description

Project Description

This is a description of a Practical Research Project associated with the PREP course

Project Title

Establishing a precise account of some novel OO language mechanisms

Quarter

Responsible

Aims

This project will explore the precise modeling of novel features in object-oriented language semantics and type systems using the proof assistant Coq. One important case which could form the basis for this effort is the ObjectTeams language, which includes such concepts as lifting and lowering that enable a pair of objects with entirely unrelated types to work almost like a single object with several types. The goal is then to clarify a simple core of the semantics and type system, and (if time permits) to show that the type system is sound.

Learning Outcome

Learning about the new mechanisms through literature studies and/or experiments with running language implementations
Producing a more foundational view on the mechanisms under scrutiny
Developing a deeper understanding of the nature of mechanized proofs

Requirements

The TOOL course or similar courses yielding some insight into formalizations of programming languages.