Student research opportunities

Proofs, Not Programs!

Project Code: CECS_1105

This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD

Keywords:

Constructive Logic, Program Extraction, Program Correctness, Verification

Supervisor:

Dr Dirk Pattinson

Outline:

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 of this project

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/Prerequisites

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

Student 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.

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/.

Contact: