Programming Language Theory Based on Logical Methods

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

Our purpose of the research was applications of logic, in particular proof-theory, to programming language theory. We especially gave a special attention on linear logic, higher-order term rewriting and type theory. In this research project, we gave a general framework of proof-normalization (and cut-elimination) proofs from the both semantical and syntactical points of view. Then we applied our proof-normalization theorems to give computation models for various new programming languages and formal specification languages. Our new proof-normalization (and cut-elimination) theorems provide(s) logical computation models for various logical programming languages, including strongly-typed functional programming languages, executable algebraic (equational) specification languages, logic programming languages, some of concurrent process calculus languages, and their combinations. In particular, we gave a logical computation model for a combined language of typed lambda calculus with inductive type inferences and with higher order rewritings, which resulted in a new multi-paradigm programming language with both the paradigm of typed functional programming language and the paradigm of algebraic specification language. We also gave computation models for proof-search based-verification systems, including verification systems for concurrent process specification languages and for real-time multi-agent system specification languages.