CAREER: DELPHIN: Functional Programming in Logical Frameworks

点击翻译按钮获取中文摘要

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