Skip to Main content Skip to Navigation

Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage

Abstract : This thesis is about the combination of lambda-calculus with rewriting. We mainly study two properties: confluence and strong normalization. We begin by studying under which conditions the combination of a confluent conditional rewrite relation to the lambda-calculus leads to a confluent relation. Next, we study strong normalization proofs of typed lambda-calculi that use the reducibility technique. Our main contribution is a comparison of variants of this technique, with respect to how they extend to rewriting and how they handle union and implicit existential types. Finally, we present a termination criterion for the combination of conditional rewriting and lambda-calculus based on a constrained type system. Our approach, which extends known criteria that use sized types, is to our knowledge the first termination criterion for conditional rewriting with higher-order right-hand sides that takes into account in the termination argument some information generated by the satisfaction of the conditions of the rewrite rules
Complete list of metadata

Cited literature [50 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 2:01:40 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


Files produced by the author(s)


  • HAL Id : tel-01752911, version 1



Colin Riba. Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2007. Français. ⟨NNT : 2007INPL102N⟩. ⟨tel-01752911⟩



Record views


Files downloads