Application of type theory and linear logic for Programming Languages
| Project/Area Number |
07044093
|
|---|
| Research Category |
Grant-in-Aid for international Scientific Research
|
| Allocation Type | Single-year Grants |
|---|
| Section | Joint Research |
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
OKADA Mitsuhiro Keio University, Professor, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HAYASHI Susumu Kobe University, 工学部, 教授 (40156443)
TAKAHASHI Masako Tokyo Institute of Technology, 理学部, 助教授 (00015588)
OHORI Atsushi Kyoto University, 数理解析研究所, 助教授 (60252532)
HAGIYA Masami Tokyo University, 理学部, 教授 (30156252)
SATO Masahiko Kyoto University, 工学部, 教授 (20027387)
PARIGOT Michel Universite Paris VII
HUET Gerard INRIA,France
JOUANNAUD Jean-Pierre Universite Paris XI,L.R.I.
CURIEN Pierre-Luis Ecole Normale Superiuer-Paris
GIRARD Jan-Yves CNRS Mathematics Instutute-Marseille
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Project Status |
Completed (Fiscal Year 1996)
|
| Budget Amount *help |
¥10,200,000 (Direct Cost: ¥10,200,000)
Fiscal Year 1996: ¥5,100,000 (Direct Cost: ¥5,100,000)
Fiscal Year 1995: ¥5,100,000 (Direct Cost: ¥5,100,000)
|
|---|
| Keywords | Type Theory / Linear Logic / Constructive Proof / Programming Languages / Program Verification / Program Semantics / Concurrency / Intuitionistic Logic / Proof Theory / 直観主義理論 / プログラム言語 |
|---|
| Research Abstract |
Type THeory is provides an ideal formal framework for program verification and systematic program development utililzing the logical mechanism. On the other hand, linear logic provides the framework for expressing computational resources and concurrent computation. Therefore, it seems very promising to combine these two theories in order to design a powerful and new programming language and its program development tools. For this purpose, we have investigated the theoretical foundations for this combined formal framework, linear type language.
In particular, we established verious important semantics theories for the linear type language. For example, phase semantics is extended to a dynamic phase semantics in which cut-elimination and normalization proofs can be performed. Phase semantics is also extended to higher order linear type languages. Girard introduced Light Linear Logic, which is considered an impotant sybsystem of linear logic since it characterized the polynomial time computation in a purely logical way. We applied our phase semantics theory to Light Linear Logic and established phase semantic characterization of the important concepts used in Light Linear Logic. The coherence semantics has also been very much improved. For example, Coherence Banach Space Semantics, which is a promising denotational semantics for the linear type language, was developped when the French team leader, J-Y.Girard, visited our group in Japan. Various important computation models for the linear type language have been proposed in our project research. In particular, the reduction paradigm and the proof-search paradigm were studied from the programming paradigm and the proof- search paradigm were studied from the programming languages point of view.
|
Report
(3 results)
Research Products
(46 results)
