MastersThesis
Master Thesis Proposals
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
Semantics of programming languages in Agda (a la Bertot in Coq).
contact person: Ana Bove
Programming language support for a course on Type Systems
A course on type systems for programming languages covers both a number of formal systems (computation rules, type systems) and algorithms (evaluators, simplifiers, type checkers). It is very useful for a student to experiment with these notions by implementing them in a programming language. Functional languages are suitable for implementing these algorithms. But if the functional language is equipped with dependent types, then the type system can be used also to specify computation rules and type systems, and thus to express correctness properties of the algorithms.
In this project the task is to develop such support for the course on Types for Programs and Proofs - an advanced course at Chalmers. This course uses the book "Types and Programming Languages" by Benjamin Pierce: http://www.cis.upenn.edu/~bcpierce/tapl/index.html .
The task is to use the programming language Agda developed at Chalmers for implementing a number of notions covered by Pierce. In Pierce's course, given at the University of Pennsylvania, the Coq system is used for a similar purpose. The thesis is expected to contain a comparison between Agda and Coq for this purpose.
contact person: Peter Dybjer
Translating Haskell into Agda using domain predicates or coinductive types following Bertot.
contact person: Ana Bove
Exact real number computation in Agda
When computing, real numbers are usually approximated by floating point numbers, and it is then necessary to keep the resulting round off errors under control. An alternative approach is however to work with exact computable real numbers. These are infinite sequences (for example Cauchy sequences) which provide arbitrarily close approximations of the number. These sequences are then be implemented as functions or as lazy lists. See for example http://www.dcs.ed.ac.uk/home/mhe/plume/index.html which shows how to implement exact real number computations using streams in Haskell.
Agda is a functional programming language with dependent types. Its type system is more expressive than Haskell, and gives the user the possiblility to express more or less arbitrary logical properties.
The task of this project is to develop a library of functions on real numbers in Agda, and to use the type system to express simple properties on them. Such a library could be used for teaching beginning university students about real numbers and the elements of calculus. In a futuristic approach to teaching, we envisage freshman level mathematics being taught together with functional programming, logic, and numerical analysis. Part of the project could involve thinking about how such a curriculum could be structured.
There is already a substantial literature on the topic of exact real number computations, both in connection with functional languages and in connection with dependent types.
contact person: Peter Dybjer
Dependent type theory and imperative computation
Many efficient algorithms rely on low-level management of memory, such as pointer manipulation. Originally, such low-level management was not available in functional programming languages. However, in modern functional programming languages such as ML and Haskell, it is possible to integrate it with ordinary functional computations. In ML the type system is extended with reference types and new constructs for manipulating references. In Haskell monads are used to encapsulate computation which is impure from the functional point of view. For example, stateful computation is encapsulated using the state monad.
When programming in a functional language with dependent types, such as the Agda languages developed at Chalmers, we would also like to have access to low-level manipulation of memory in a similar way as in Haskell or as in ML. However, the rich types system provided by dependent types provides new possibilities. For example, we an now express logical pre- and post-conditions using types. However, it is not so clear how to keep the resulting logical complexity under control. It is a current hot topic to integrate dependent types and stateful computation. Two of the main research efforts in this direction is the Hoare Type Theory developed by Gregg Morrisette at Harvard, and the Krakatoa System developed by Christine Paulin at Paris Sud.
In this project we would like to investigate how such ideas could be integrate in the Agda language. Libaries for imperative computations using state monads could be developed. New axioms a la those of Hoare Type Theory could be considered.
contact person: Peter Dybjer
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