• View
• Edit
• History
• Print

QuantifierEliminationAndFunctionalProgramming

Quantifier Elimination and functional programming

Quantifier elimination is a fundamental technique in mathematical logic and computer science (see the corresponding article in wikipedia). It is a technique which shows the decidability of several logical theories, important for applications (linear orders, Presburger arithmetic, algebraically closed fields, real closed fields). In a recent work http://www4.informatik.tu-muenchen.de/~nipkow/pubs/MOD2007.html Tobias Nipkow shows that it is possible to implement this technique in an elegant way in a functional programming language, and to prove the correctness formally in the theorem prover Isabelle.

The goal of this project is to transfer these programs in the dependently types programming language Agda. The representation should even be more elegant, and can then be used to integrate powerful decision procedures in Agda and to test its efficiency.

A familiarity with logic and functional programming is recommended.

contact person: Thierry Coquand