Bibliografías temáticas / Multiplicative-additive linear logic

Índice

  1. Artículos de revistas
  2. Tesis
  3. Capítulos de libros

Literatura académica sobre el tema "Multiplicative-additive linear logic"

Autor: Grafiati
Publicado: 14 de diciembre de 2024

Crea una cita precisa en los estilos APA, MLA, Chicago, Harvard y otros

Elija tipo de fuente:

Consulte las listas temáticas de artículos, libros, tesis, actas de conferencias y otras fuentes académicas sobre el tema "Multiplicative-additive linear logic".

Junto a cada fuente en la lista de referencias hay un botón "Agregar a la bibliografía". Pulsa este botón, y generaremos automáticamente la referencia bibliográfica para la obra elegida en el estilo de cita que necesites: APA, MLA, Harvard, Vancouver, Chicago, etc.

También puede descargar el texto completo de la publicación académica en formato pdf y leer en línea su resumen siempre que esté disponible en los metadatos.

Artículos de revistas sobre el tema "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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Resumen
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
Los estilos 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.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.

Tesis sobre el tema "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.

Texto completo
Resumen
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
Los estilos APA, Harvard, Vancouver, ISO, etc.

Capítulos de libros sobre el tema "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.

Texto completo
Los estilos 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.

Texto completo
Resumen
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.
Los estilos 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.

Texto completo
Los estilos APA, Harvard, Vancouver, ISO, etc.
Ofrecemos descuentos en todos los planes premium para autores cuyas obras están incluidas en selecciones literarias temáticas. ¡Contáctenos para obtener un código promocional único!

Pasar a la bibliografía