Functional logic languages seamlessly integrate the most appealing features of the functional and the logic paradigms: independence from evaluation order, higher-order functions, and polymorphic typing from the functional paradigm, and evaluation with partial information (logic variables), constraint solving, and non-deterministic search for solutions from the logic paradigm. Unfortunately, compiling a language with this rich combination of features is a difficult problem. Code generators of current compilers for functional logic languages are complicated ad-hoc modules that, with two exceptions, do not even attempt to address in a disciplined way the correctness of the generated code or relate its performance to that of the source code. The exceptions state the correctness in a very weak, double negative form: no result of a source program is not producible by the object program.
This project is for the design and implementation of a disciplined compiler for the functional logic language Curry. The generated code will be abstract and easily mappable to common programming languages and hardware architectures, and will be formally defined and proved correct. In particular, every result of a source program will be produced by the object program. The steps executed by the generated code will be closely related to the needed steps in a formal model of the source code. This will ensure that program executions will be more predictable and as efficient as theoretically possible. The code produced by the research will be available to the research community as part of a modern compiler for Curry.
