Formally Verified Bug-free Implementations of (Logical) Algorithms
The aim of this project is to develop formally verified functional implementations of classical logical algorithms like the Horn satisfiability. Concretely, the objective is twofold: - the functional implementation of classical logical algorithms as showcases of clean and clear code close to specifications; - the development of correctness proofs of the implementations as showcases of the feasibility and usability of machine-checked program proof systems.

OCaml-Flat on the Ocsigen framework
Develop a graphical interface for OCaml-Flat using the Ocsigen framework. Other similar systems, such as JFLAP, should be studied. The main general functionalities: Edition of finite automata, push-down automata and Turing machines, displayed as graphs; Visualization of generation processes; and Visualization of recognition processes, given an input string.

Continuation-Passing Style for automatic program instrumentation
Modern optimizer compilers can automatically transform functions with complex patterns of use of Call Stack in functions that operate in constant space on the call stack. Particular cases of these are, for well behaved terminal recursive functions. A powerful technique for performing this operation is called continuation passing style (CPS) transformation. The purpose of this project is to implement such a mechanism as a OCaml programming language extension that operates automatically via a particular extension of the syntax.

OCaml-Flat - An OCaml Toolkit for experiment with formal languages theory
Develop a FLAT toolkit to support the definition of alphabets, order relations and languages. The languages will be mainly defined using language generators and language recognizers. Here are some definitional mechanisms to support: predicates (Boolean functions), regular expressions, finite automata, context-free grammars, push-down automata, Turing machines.