CAREER: DELPHIN: Functional Programming in Logical Frameworks

职业：delphi：逻辑框架中的函数式编程scarsten schuermann数据结构，如列表，树，图，数组以及对它们的操作是计算机科学中研究最多的概念之一，并得到大多数现代编程语言的支持。另一方面，定理、证明和推导在表达性逻辑框架中具有优雅的表示，但即使在现代编程语言中，通常也会导致复杂、复杂和最终不可靠的编码。拟议的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#.