Algorithms for Modal Types




The extension of typed programming languages with type-formers called 'modalities' is an active current area of research. For example, modalities can give the programmer more fine-grained control over when code is executed, and hence avoid erroneous recursive definitions which try to use data which cannot yet have been produced. To be useful, typed programming languages need algorithms that can check whether a given program has the type claimed, or even try to infer the type of a given program. This project involves implementing algorithms to check or infer types for a basic notion of typed functional programming language known as the simply typed lambda-calculus, extended with a modality.


The student will write a program that can either check, or infer, types for the simply typed lambda-calculus with a basic notion of modality. Depending on the level and interests of the student, and the time available for the project, the student could extend this work by considering more advanced language properties such as sums and polymorphism, or more advanced notions of modality, or by proving the soundness of the algorithm.


The student will be a competent programmer with an interest in logic and/or principles of programming languages. Familiarity with the lambda-calculus, or with natural deduction, would be a plus but is not essential.


This project is intended to introduce the student to concepts of current research interest in types, logic, and programming languages, and so will be of particular interest to students interested in pursuing research in these areas.

Updated:  10 August 2021/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing