Explicit resources from the rewriting point of view.
type: Dataset
description: This thesis deals with the management of explicit resources in functional languages, stressing on properties of calculi with explicit substitutions refining the lambda-calculus. In the first part, we are concerned with the preservation property of beta-strong normalisation (PSN) for the lambda s-calculus, a language among the eight calculi of the prismoid of resources defined thereafter. In the second part, we study the confluence property for a large set of calculi with explicit substitutions. After having given a generic proof of confluence based on a series of axioms that a calculus must fulfill to verify this property, we focalise on the metaconfluence of lambda j, a calculus where the propagation mechanism of substitutions uses the notion of multiplicity, whereas the traditional way is the structural propagation. In the third part, we define a prismoid of resources which generalise in a parametric way the lambda-calculus in the sense that not only the substitution can be explicit, but also the contraction and the weakening. This gives a set of eight calculi spread over the vertices of the prismoid for which we prove in a uniform way several properties of good behavior as the simulation of beta-reduction, PSN, confluence, and strong normalisation for typed terms. In the last part of the thesis we show different opening up to more practical domains. First, we are concerned with the complexity of a calculus with substitutions. We present research tools and conjecture on maximal bounds for reductions of the lambda x-calculus . Finally, we give a formal specification of the lambda j-calculus within the proof assistant Coq.
issued: 2026-05-18T20:40:34.290421
language: fr
modified: 2026-05-18T20:40:34.290427
contact point: Organization
  fn: CCSD
keyword: complexite
keyword: formalisation
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-flcomputer-science-csformal-languages-and-automata-theory-csfl
keyword: metaconfluence
keyword: ressources
keyword: substitutions-explicites
keyword: theses
landing page: https://theses.hal.science/tel-00697408

Explicit resources from the rewriting point of view.
type: Distribution
format: HTML
issued: 2026-05-18T20:40:34.321616
modified: 2026-05-18T20:40:34.262723
access URL: https://theses.hal.science/tel-00697408

test_moissonnage_selune
type: Agent