34 citations
- Laboratoire de Mesure du Carbone 14FR9 papers
- Institut national de recherche en sciences et technologies du numériqueFR5 papers
- Université Paris-SaclayFR5 papers
- Centre National de la Recherche ScientifiqueFR4 papers
- École Normale Supérieure Paris-SaclayFR4 papers
- École PolytechniqueFR4 papers
- Mathématiques et Informatique pour la Complexité et les Systèmes3 papers
- CentraleSupélecFR2 papers
- Centre Inria de SaclayFR2 papers
- Laboratoire d'Informatique de l'École PolytechniqueFR2 papers
- Aix-Marseille UniversitéFR1 paper
- Atos (France)FR1 paper
Showing 2015Show all
2 papers · 1 filter
cs.LO2015★ 12 cited
The computability path ordering
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability pa…
cs.LO2015
Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)
Ali Assaf
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…