@prefix dcat: <http://www.w3.org/ns/dcat#> .
@prefix dct: <http://purl.org/dc/terms/> .
@prefix foaf: <http://xmlns.com/foaf/0.1/> .
@prefix vcard: <http://www.w3.org/2006/vcard/ns#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-tel-00697408v1> a dcat:Dataset ;
    dct: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.
            """ ;
    dct:identifier "tel-00697408" ;
    dct:issued "2026-05-18T20:40:34.290421"^^xsd:dateTime ;
    dct:language "fr" ;
    dct:modified "2026-05-18T20:40:34.290427"^^xsd:dateTime ;
    dct:publisher <https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> ;
    dct:title "Explicit resources from the rewriting point of view." ;
    dcat:contactPoint [ a vcard:Organization ;
            vcard:fn "CCSD" ] ;
    dcat:distribution <https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-tel-00697408v1/resource/7a231d8b-3183-496c-940a-22864a9d67e7> ;
    dcat:keyword "complexite",
        "formalisation",
        "infoeu-reposemanticsdoctoralthesis",
        "infoinfo-flcomputer-science-csformal-languages-and-automata-theory-csfl",
        "metaconfluence",
        "ressources",
        "substitutions-explicites",
        "theses" ;
    dcat:landingPage <https://theses.hal.science/tel-00697408> .

<https://rec.harvest-normandie.data4citizen.com/dataset/oai-hal-tel-00697408v1/resource/7a231d8b-3183-496c-940a-22864a9d67e7> a dcat:Distribution ;
    dct:format "HTML" ;
    dct:issued "2026-05-18T20:40:34.321616"^^xsd:dateTime ;
    dct:modified "2026-05-18T20:40:34.262723"^^xsd:dateTime ;
    dct:title "Explicit resources from the rewriting point of view." ;
    dcat:accessURL <https://theses.hal.science/tel-00697408> .

<https://rec.harvest-normandie.data4citizen.com/organization/cce9db95-46d9-4dc2-84b6-764215d0a002> a foaf:Agent ;
    foaf:name "test_moissonnage_selune" .

<https://theses.hal.science/tel-00697408> a foaf:Document .