Skip to Main content Skip to Navigation
New interface

Typage et déduction dans le calcul de réécriture

Abstract : The rewriting calculus is a lambda-calculus with pattern matching. This thesis is devoted to the study of type systems for this calculus, and to its use in the domain of deduction. We study two typing paradigms. The first one is inspired by the simply-typed lambda-calculus, but it differs from it in the sense that a term may be well-typed without being terminating. Thus, we use it for representing programs and rewriting systems. The second family of type systems we study is adapted from the Pure Type Systems. We show its strong normalization via a translation into a typed lambda-calculus. Finally, we propose two ways of using the rewriting calculus in logic. In the first approach, we use the strongly normalizing systems to define proof terms for deduction modulo. In the second, we define a generalization of natural deduction and we show that matching is useful in order to represent the rules of this deduction system.
Document type :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:40:04 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Intranet access


  • HAL Id : tel-01746546, version 1



Benjamin Wack. Typage et déduction dans le calcul de réécriture. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2005. Français. ⟨NNT : 2005NAN10119⟩. ⟨tel-01746546⟩



Record views