CAREER: DELPHIN: Functional Programming in Logical Frameworks

职业：DELPHIN：逻辑框架中的函数式编程

• 批准号: 0133502
• 负责人: Carsten Schuermann
• 金额: $ 30万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-02-01 至 2007-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0133502&HistoricalAwards=false
• 关键词: CAREER; DELPHIN; Functional; Programming; Logical

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#.

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