研究課題
基盤研究(C)
置換簡約の強正規化可能性は近年活発に研究されている。また、定理自動証明システムCoqは、フランスで研究開発されている証明システムで、基本理論と応用の両面で成功している。本研究では、これらの研究成果を深化発展させることにより、置換簡約の型理論の研究を行う。
すべて 2010 2009
すべて 雑誌論文 (3件) (うち査読あり 3件)
ACM Transactions on Computational Logic (to appear)
\em Annals of Pure and Applied Logic (to appear)
Lecture Notes in Computer Science 5771
ページ: 470-484