Proofs, Not Programs!

Research areas

Temporary Supervisor

Dr Dirk Pattinson


Program extraction is a technique for creating programs from proofs. For example, instead of implementing a function that sorts a list, one proves that for every list, there exists a second, sorted list with the same entries. Program extraction then turns this into a program, and also generates a proof that this program is correct. We have developed a new approach to analysis, based on domain theory, that is particularly suitable for this approach.


The goal is to implement some proofs of theorems or facts in (constructive) analysis in a theorem prover, and then to analyse, compare and benchmark the programs with respect to other approaches.


Background in formal logic. Familiarity with (very) basic Analysis and theorem provers a plus.

Background Literature

The proofs should be implemented in the Minlog system, developed at Munich University, and the basics are explaiend in the Minlog turorial, available via


In-depth knowledge and hands-on experience in constructive logic, program extraction and (very basic) mathematical analysis. The project could well lead to a publication and/or PhD thesis.

Updated:  1 June 2019/Responsible Officer:  Head of School/Page Contact:  CECS Marketing