SHF: Small: A principled compiler for functional logic languages

函数逻辑语言无缝地集成了函数和逻辑范式中最吸引人的特性：独立于函数范式的求值顺序、高阶函数和多态类型，以及使用部分信息（逻辑变量）求值、约束求解和从逻辑范式中寻找解决方案的非确定性搜索。不幸的是，编译具有如此丰富特性组合的语言是一个难题。函数式逻辑语言的当前编译器的代码生成器是复杂的特殊模块，除了两个例外，它们甚至不试图以一种有纪律的方式解决生成代码的正确性或将其性能与源代码的性能联系起来。异常以一种非常弱的双重否定形式声明正确性：源程序的任何结果都不能由目标程序产生。这个项目是为功能逻辑语言Curry设计和实现一个有纪律的编译器。生成的代码将是抽象的，并且易于映射到公共编程语言和硬件架构，并且将被正式定义并证明是正确的。特别地，源程序的每个结果都将由目标程序产生。生成的代码执行的步骤将与源代码的正式模型中所需的步骤密切相关。这将确保程序的执行更加可预测，并且在理论上尽可能高效。研究产生的代码将作为Curry现代编译器的一部分提供给研究社区。

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.