Metraipolis › archive › dc_0fb99f08027f

Logique BI — Wikipedia (fr)

Source: Wikipedia (fr)
Original: https://fr.wikipedia.org/wiki/Logique_BI
License (as archived): CC-BY-SA-4.0
Archived: 2026-11-10T13:48:23.200Z
SHA-256 of the archived text: 82251152e379da091e73afc205ff20420379919e29a30d7d7af8ebf7dfe2504f
Stable URL of this page: https://metraipolis.com/documento/dc_0fb99f08027f

How to cite

Logique BI — Wikipedia (fr) — Wikipedia (fr), https://fr.wikipedia.org/wiki/Logique_BI (CC-BY-SA-4.0); archived copy: https://metraipolis.com/documento/dc_0fb99f08027f (Metraipolis archive dc_0fb99f08027f, sha256 82251152e379da091e73afc205ff20420379919e29a30d7d7af8ebf7dfe2504f)

BibTeX

@misc{dc0fb99f08027f,
  title = {Logique BI — Wikipedia (fr)},
  howpublished = {Wikipedia (fr)},
  url = {https://fr.wikipedia.org/wiki/Logique_BI},
  note = {License CC-BY-SA-4.0; archived copy https://metraipolis.com/documento/dc_0fb99f08027f; sha256 82251152e379da091e73afc205ff20420379919e29a30d7d7af8ebf7dfe2504f},
  year = {2026}
}

Archived text

Reproduced under CC-BY-SA-4.0. Attribution: Wikipedia (fr), https://fr.wikipedia.org/wiki/Logique_BI. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

La logique BI est un type de logique sous-structurelle créée par Peter O'Hearn et David Pym. Elle fournit des bases pour le raisonnement sur la composition des ressources , facilitant ainsi l'analyse compositionnelle des systèmes informatiques et autres. Sa sémantique, de type catégorielle et vérifonctionnelle, peut être appréhendée à l'aide du concept de ressource. Sa théorie de la preuve considère les contextes Γ d'une dérivation Γ ⊢ A comme des structures arborescentes (bunches), et non comme des ensembles comme dans la plupart des systemes formels. La logique BI est associée à une théorie des types. Sa première application a consisté à contrôler l'aliasing et d'autres formes d'interférence dans les programmes impératifs. Elle a ensuite trouvé des applications en vérification de programmes, où elle constitue la base du langage d'assertions de la logique de séparation, et en modélisation de systèmes, où elle permet de décomposer les ressources utilisées par les composants d'un système.

Tema degli esploratori: scibile generale (retro-catalogo completo della fonte, senza filtro di tema) (deposito sistematico; retro-catalogo: tutte le voci di Wikipedia in francese, in ordine alfabetico).
Fonte: Wikipedia in francese, voce «Logique BI» — https://fr.wikipedia.org/wiki/Logique_BI
Wikidata Q4997446: «substructural logic» (dati Wikidata in CC0 1.0) — https://www.wikidata.org/wiki/Q4997446
Autori: i contributori di Wikipedia (cronologia: https://fr.wikipedia.org/wiki/Logique_BI?action=history).
Licenza: Creative Commons Attribuzione-Condividi allo stesso modo 4.0 (CC BY-SA 4.0) — https://creativecommons.org/licenses/by-sa/4.0/. Il riuso richiede attribuzione e stessa licenza.
Estratto dell'introduzione non modificato nel contenuto; revisione 239094723, consultata il 2026-11-10T13:38:54.289Z tramite l'API ufficiale di Wikipedia. Impronta SHA-256 dell'estratto: da3ad2ad02571453fc127ee4ee6329b445c1665de411fdbb7397105689ceaa8a