Skip to Main content Skip to Navigation
Theses

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 metadatas

Cited literature [50 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01752911
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 2:01:40 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:10 PM

File

2007_RIBA_C.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01752911, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

54

Files downloads

35