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