School of Electronic Engineering and Computer Science

Programs and Proofs

Supervisor: Dr Paulo Oliva

Research group(s): Theory


This project aims to apply techniques of mathematical logic and proof theory in the extraction of correct programs from proofs. The main tools used are proof translations and proof transformations, e.g.

A good knowledge of propositional and predicate logic is necessary. For more papers in the areas see: