Hybrid Linear Logic, revisited

Abstract : 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 judgments 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 extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (µHyMALL), which can be encoded into multiplicative additive linear logic with fixed points (µMALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both µMALL and µHyMALL. In the former, states are represented as atoms in the linear context, hence reflecting a more operational view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the semantics of CTL.
Document type :
Journal articles
Complete list of metadatas

Contributor : Kaustuv Chaudhuri <>
Submitted on : Wednesday, January 2, 2019 - 10:50:49 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Wednesday, April 3, 2019 - 2:42:46 PM


Files produced by the author(s)


  • HAL Id : hal-01968154, version 1


Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, Cambridge University Press (CUP), In press. ⟨hal-01968154⟩



Record views


Files downloads