CAREER: DELPHIN: Functional Programming in Logical Frameworks

CCR-0133502 CAREER：Delphin：逻辑框架中的函数式编程Carsten Schuerman数据结构，如列表、树、图、数组以及对它们的操作是计算机科学中研究最多的概念之一，并得到大多数现代编程语言的支持。另一方面，定理、证明和推导在表达逻辑框架中具有优雅的表示，但通常导致复杂、复杂的编码，甚至在现代编程语言中也是如此。建议的Delphin项目致力于如何将编程语言的计算特征与逻辑框架的表示特征结合在一起的基础研究。在Delphin中，程序员可以用优雅而紧凑的数据对象编写自动化的定理证明器、解释器和编译器，这些对象表示类型派生(用于编译器)、证明(用于携带代码的证明)和计算痕迹(用于抽象机器)。该项目运用了高阶理论、依赖类型、元逻辑框架和函数式程序设计语言的技术。Delphin将阐明抽象概念与其表示之间的认识论张力，并将提供关于它们的操作的答案。此外，它还将开辟新的研究领域，研究如何将逻辑框架技术融入其他主流编程语言，如Java和C#。

CCR-0133502CAREER: Delphin: Functional Programming in Logical FrameworksCarsten SchuermannData structures such as lists, trees, graphs, arrays along withoperations on them are one of the most studied concepts in computerscience and supported by most modern programming languages. Theorems,proofs, and derivations on the other hand have elegant representationsin expressive logical frameworks but lead in general to complicated,convoluted, and ultimately unreliable encodings even in modernprogramming languages.The proposed Delphin project engages in fundamental research on how tobring together the computational features of programming languageswith the representational features of logical frameworks. In Delphinprogrammers can write automated theorem provers, interpreters, andcompilers with elegant and compact data objects representing typingderivations (for compilers), proofs (for proof carrying code), andcomputation traces (for abstract machines). The proposed projectemploys techniques from higher-order theories, dependent types,meta-logical frameworks, and functional programming languages.Delphin will shed some light on the epistemological tension betweenabstract concepts and their representations; and it will provideanswers concerning their manipulation. Moreover, it will open up newresearch areas of how to incorporate logical framework technology intoother mainstream programming languages such as Java and C#.