Proofs, Not Programs!

Research areas

Temporary Supervisor

Dr Dirk Pattinson

Description

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.

Goals

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.

Requirements

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 http://www.minlog-system.de/.

Gain

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