Nicolas Max David Münnich

Addressing machines have been introduced as a formalism to construct models of the pure, untyped λ-calculus. We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls. We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions. Finally, we show that they are also well suited for representing regular PCF programs (closed terms) computing natural numbers.

Weighted relational models are a way of extracting a diverse amount of information from a program through the enhancement of relational models. In this work weighted relational models are extended to the simply typed lambda-calculus, presenting a method of extracting information from the model using an enhanced simply typed lambda-calculus. The quality of the information extracted is also discussed by analysing to which degree the values are precisely calculable and to which degree they can only be approximated.

Basic SCI is a programming language grounded in mathematical theory, with few implementations created around it. This project is on generating a complete representation of a Basic SCI program using a fully abstract trace based mathematical model developed by G. McCusker. Of particular note is the work done on abstraction over numbers and the various challenges and solutions involved.