文章基本信息

标题：Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting
本地全文：下载
作者：Ali Assaf
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：38
页码：31-44
DOI：10.4230/LIPIcs.TLCA.2015.31
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.
关键词：lambda Pi calculus modulo rewriting; pure type systems; logical framework; normalization; conservativit