Applications of Type Theory and Linear Logic to Programming Language Theory

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

Our purpose of the research was applications of type theory, intuitionistic logic and linear logic to programming language theory. We first gave various fundamental researches of semantics and the proof-normalization and proof-search techniques for type theory (equivalently, intuitionistic logic, under the Curry-Howard correspondence) and linear logic, which provided computation models of our new programming and specification/verification languages. In particular, we gave a logical computation model for a combined language of type theory with linear logic, which resulted in a new multi-paradigm programming language with both the paradigm of typed functional programming language and the paradigm of concurrent process calculus. 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. In particular, we gave PSPACE-decidability result for verifications of safety and other important properties of real-time finite state system specifications based on our linear logic-based formal specification language.