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.

• Unifying functional interpretations

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

• Proof Mining: A Systematic Way of Analyzing Proofs in Mathematics
• Proof mining in L1 approximation