2026-07-22T20:49:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5153 2024-03-06T10:36:09Z ddc:004 open_access

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting Assaf, Ali lambda Pi calculus modulo rewriting pure type systems logical framework normalization conservativit 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ali Assaf 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.31 urn:nbn:de:0030-drops-51535 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31 eng https://creativecommons.org/licenses/by/3.0/legalcode