Dissymetrical Linear Logic
Résumé
This paper is devoted to design computational systems of linear logic (i.e. systems in which, notably, the non linear and structural phenomena which arise during the cut-elimination process are taken in charge by specific modalities, the exponentials: ! and ?). The systems designed are "intermediate" between Intuitionistic LL and Classical LL. Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in Classical LL-and this without to loose the computational properties (closure by cut-elimination, atomizability of axioms). Three main systems are designed (Dissymetrical LL, semi-functorial Dissymetrical LL, semi-specialized Dissymetrical LL), where, in each of them, ! and ? play well differentiated roles.
Origine : Fichiers produits par l'(les) auteur(s)