Metaconfluence of λj: dealing with non-deterministic replacements

This paper focuses on the λj-calculus, a formalism with jumps inspired from linear logic, and based on the notion of multiplicity. We consider terms with metavariables, and we prove metaconfluence of the calculus equipped with an equivalence relation. This confers to λj all the good properties that one can expect.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00926488
Author Renaud, Fabien
Maintainer CCSD
Last Updated May 7, 2026, 13:50 (UTC)
Created May 7, 2026, 13:50 (UTC)
Identifier hal-00926488
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
creator Renaud, Fabien
date 2011-05-07T00:00:00
harvest_object_id 67d0c0f0-d7b1-4542-b6fb-6a354c31a612
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2023-03-24T00:00:00
set_spec type:UNDEFINED