Conservativity of embeddings in the lambda-Pi calculus modulo rewriting (long version)

Abstract : The lambda-Pi calculus can be extended with rewrite rules to embed any other functional pure type system. The normalization and conserva-tivity properties of the embedding is an open problem. In this paper, we show that the embedding is conservative. We define an inverse translation into a pure type system completion and show that the completion is con-servative using the reducibility method. This result further justifies the use of the lambda-Pi calculus modulo rewriting as a logical framework.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-01084165
Contributeur : Ali Assaf <>
Soumis le : lundi 20 avril 2015 - 19:15:00
Dernière modification le : mercredi 14 décembre 2016 - 01:07:11
Document(s) archivé(s) le : mercredi 19 avril 2017 - 00:41:32

Fichier

conservativity-embeddings-long...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : hal-01084165, version 3
  • ARXIV : 1504.05038

Collections

Citation

Ali Assaf. Conservativity of embeddings in the lambda-Pi calculus modulo rewriting (long version). 2015. <hal-01084165v3>

Partager

Métriques

Consultations de
la notice

150

Téléchargements du document

89