• View
• Edit
• History
• Print

ConstructiveAlgebraInFunctionalProgrammingAndTypeTheory

Constructive algebra in functional programming and type theory

One of the first application of LISP was to write some symbolic algorithms in algebra, and one could expect close connections between computer algebra and functional programming. Surprisingly however, relatively few works in functional programming relate to computer algebra.

In this project we will explore some of these connections on the example of Prufer domains. This is a simple notion, that can be caracterised by a simple first-order condition. Several basic algorithms in number theory and algebraic curves can be expressed at the level of Prufer domains. The project will involve a representation of these algorithms, first in Haskell, then in a functional programming with dependent types so that we can represent proofs as well and get a nicer representation of algebraic structures.

Functional programming and a basic knowledge in algebra (what is a ring) are prerequisite.

contact person: Thierry Coquand