A Case Study on Imperative Program Extraction

Gregory Woods

(Swansea University)

The process of program extraction has long been associated with functional programs with little research in the direction of imperative program extraction. While many useful tools exist to extract functional programs (Agda, Isabelle, Coq and NuPRL) the simple fact is that most programs that are written are more towards the imperative paradigm.

In this talk we explore a case study which demonstrates that imperative program extraction is possible. The problem we choose to solve using this method is the classic problem of sorting a list of numbers. Many algorithms exist to solve this problem and we will focus on one of the most famous, Quicksort. We present a successful attempt at extracting a program, that yields imperative behaviour, from a constructive proof. The software used for this is the interactive theorem prover Minlog.

Thursday 7th March 2013, 14:00
Robert Recorde Room
Department of Computer Science