SHF: Small: A principled compiler for functional logic languages

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

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.