Systèmes de types purs et substitutions explicites

Pure type systems are a generic formalism for usual lambda-calculus, which combine great simplicity and elegance to a high expressivity power. This thesis sudies various extensions of this notion, mostly to calculi with explicit substitutions, and to classical sequent calculi, with a particular focus on the preservation of the good properties of these systems.Les systèmes de types purs sont un formalisme générique au pouvoir d'expressivité élevé, dont l'élégance et la sobriété sont grandes, pour le lambda-calcul usuel. Cette thèse étudie différentes extensions de cette notion de systèmes de types purs, principalement à des calculs à substitutions explicites, et à des calculs de séquents classiques, en s'intéressant particulièrement à la préservation des bonnes propriétés de ces systèmes