Bibliographies thématiques / Multiplicative-additive linear logic

Sommaire

  1. Articles de revues
  2. Thèses
  3. Chapitres de livres

Littérature scientifique sur le sujet « Multiplicative-additive linear logic »

Auteur : Grafiati
Publié le 14 décembre 2024

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les listes thématiques d’articles de revues, de livres, de thèses, de rapports de conférences et d’autres sources académiques sur le sujet « Multiplicative-additive linear logic ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Articles de revues sur le sujet "Multiplicative-additive linear logic"

1

MAZZA, DAMIANO. "Infinitary affine proofs." Mathematical Structures in Computer Science 27, no. 5 (2015): 581–602. http://dx.doi.org/10.1017/s0960129515000298.

Texte intégral
Résumé :
Even though the multiplicative–additive fragment of linear logic forbids structural rules in general, is does admit a bounded form of exponential modalities enjoying a bounded form of structural rules. The approximation theorem, originally proved by Girard, states that if full linear logic proves a propositional formula, then the multiplicative–additive fragment proves every bounded approximation of it. This may be understood as the fact that multiplicative–additive linear logic is somehow dense in full linear logic. Our goal is to give a technical formulation of this informal remark. We intro
Styles APA, Harvard, Vancouver, ISO, etc.
2

Lafont, Yves. "The undecidability of second order linear logic without exponentials." Journal of Symbolic Logic 61, no. 2 (1996): 541–48. http://dx.doi.org/10.2307/2275674.

Texte intégral
Résumé :
AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means
Styles APA, Harvard, Vancouver, ISO, etc.
3

Cockett, J. R. B., and C. A. Pastro. "A Language For Multiplicative-additive Linear Logic." Electronic Notes in Theoretical Computer Science 122 (March 2005): 23–65. http://dx.doi.org/10.1016/j.entcs.2004.06.049.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
4

O'Hearn, Peter W., and David J. Pym. "The Logic of Bunched Implications." Bulletin of Symbolic Logic 5, no. 2 (1999): 215–44. http://dx.doi.org/10.2307/421090.

Texte intégral
Résumé :
AbstractWe introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and pro
Styles APA, Harvard, Vancouver, ISO, etc.
5

CHAUDHURI, KAUSTUV. "Expressing additives using multiplicatives and subexponentials." Mathematical Structures in Computer Science 28, no. 5 (2016): 651–66. http://dx.doi.org/10.1017/s0960129516000293.

Texte intégral
Résumé :
Subexponential logic is a variant of linear logic with a family of exponential connectives – called subexponentials – that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (MSEL) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive connectives can be directly simulated by giving an encoding of propositional multipl
Styles APA, Harvard, Vancouver, ISO, etc.
6

Hughes, Dominic J. D., and Rob J. Van Glabbeek. "Proof nets for unit-free multiplicative-additive linear logic." ACM Transactions on Computational Logic 6, no. 4 (2005): 784–842. http://dx.doi.org/10.1145/1094622.1094629.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
7

CHAUDHURI, KAUSTUV, JOËLLE DESPEYROUX, CARLOS OLARTE, and ELAINE PIMENTEL. "Hybrid linear logic, revisited." Mathematical Structures in Computer Science 29, no. 8 (2019): 1151–76. http://dx.doi.org/10.1017/s0960129518000439.

Texte intégral
Résumé :
HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgements are labelled by worlds (having a monoidal structure) and hybrid connectives (at and ↓) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extensi
Styles APA, Harvard, Vancouver, ISO, etc.
8

Okada, Mitsuhiro, and Kazushige Terui. "The finite model property for various fragments of intuitionistic linear logic." Journal of Symbolic Logic 64, no. 2 (1999): 790–802. http://dx.doi.org/10.2307/2586501.

Texte intégral
Résumé :
AbstractRecently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction. and for its intuitionistic version (ILLC). The finite model property for related substructural logi
Styles APA, Harvard, Vancouver, ISO, etc.
9

Hamano, Masahiro. "A MALL geometry of interaction based on indexed linear logic." Mathematical Structures in Computer Science 30, no. 10 (2020): 1025–53. http://dx.doi.org/10.1017/s0960129521000062.

Texte intégral
Résumé :
AbstractWe construct a geometry of interaction (GoI: dynamic modelling of Gentzen-style cut elimination) for multiplicative-additive linear logic (MALL) by employing Bucciarelli–Ehrhard indexed linear logic MALL(I) to handle the additives. Our construction is an extension to the additives of the Haghverdi–Scott categorical formulation (a multiplicative GoI situation in a traced monoidal category) for Girard’s original GoI 1. The indices are shown to serve not only in their original denotational level, but also at a finer grained dynamic level so that the peculiarities of additive cut eliminati
Styles APA, Harvard, Vancouver, ISO, etc.
10

Bucciarelli, Antonio, and Thomas Ehrhard. "On phase semantics and denotational semantics in multiplicative–additive linear logic." Annals of Pure and Applied Logic 102, no. 3 (2000): 247–82. http://dx.doi.org/10.1016/s0168-0072(99)00040-8.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.

Thèses sur le sujet "Multiplicative-additive linear logic"

1

Di, Guardia Rémi. "Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic." Electronic Thesis or Diss., Lyon, École normale supérieure, 2024. http://www.theses.fr/2024ENSL0050.

Texte intégral
Résumé :
Cette thèse s'intéresse à l'égalité des preuves et des formules en logique linéaire, avec des contributions en particulier dans le fragment multiplicatif-additif de cette logique. En logique linéaire, et dans de nombreuses autres logiques (telle que la logique intuitionniste), on dispose de deux transformations sur les preuves : l'élimination des coupures et l'expansion des axiomes. On souhaite très souvent identifier deux preuves reliées par ces transformations, étant donné qu'elles le sont sémantiquement (dans un modèle catégorique par exemple). Cette situation est similaire à celle du λ-cal
Styles APA, Harvard, Vancouver, ISO, etc.

Chapitres de livres sur le sujet "Multiplicative-additive linear logic"

1

Maieli, Roberto. "Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic." In Logic for Programming, Artificial Intelligence, and Reasoning. Springer Berlin Heidelberg, 2007. http://dx.doi.org/10.1007/978-3-540-75560-9_27.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
2

Wood, James, and Robert Atkey. "A Framework for Substructural Type Systems." In Programming Languages and Systems. Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-030-99336-8_14.

Texte intégral
Résumé :
AbstractMechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions.We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.
Styles APA, Harvard, Vancouver, ISO, etc.
3

Abrusci, Vito Michele, and Roberto Maieli. "Cyclic Multiplicative-Additive Proof Nets of Linear Logic with an Application to Language Parsing." In Formal Grammar. Springer Berlin Heidelberg, 2016. http://dx.doi.org/10.1007/978-3-662-53042-9_3.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie