Data structures such as lists, trees, graphs, arrays along with operations on them are one of the most studied concepts in computer science and supported by most modern programming languages. Theorems, proofs, and derivations on the other hand have elegant representations in expressive logical frameworks but lead in general to complicated, convoluted, and ultimately unreliable encodings even in modern programming languages.
The proposed Delphin project engages in fundamental research on how to bring together the computational features of programming languages with the representational features of logical frameworks. In Delphin programmers can write automated theorem provers, interpreters, and compilers with elegant and compact data objects representing typing derivations (for compilers), proofs (for proof carrying code), and computation traces (for abstract machines). The proposed project employs techniques from higher-order theories, dependent types, meta-logical frameworks, and functional programming languages.
Delphin will shed some light on the epistemological tension between abstract concepts and their representations; and it will provide answers concerning their manipulation. Moreover, it will open up new research areas of how to incorporate logical framework technology into other mainstream programming languages such as Java and C#.
