Separability, Expressiveness, and Decidability in the Ambient Logic. - Daniel Hirschkoff; Étienne Lozes; Davide Sangiorgi (LICS, 2002)

Minimality Results for the Spatial Logics. - Daniel Hirschkoff; Étienne Lozes; Davide Sangiorgi (FSTTCS, 2003)

Adjuncts elimination in the static ambient logic. - Étienne Lozes (EXPRESS, 2003)

Elimination of spatial connectives in static spatial logics. - Étienne Lozes (Theor. Comput. Sci., 2005)

On the Expressiveness of the Ambient Logic. - Daniel Hirschkoff; Étienne Lozes; Davide Sangiorgi (Log. Methods Comput. Sci., 2006)

Elimination of quantifiers and undecidability in spatial logics for concurrency. - Luís Caires; Étienne Lozes (Theor. Comput. Sci., 2006)

Towards Model-Checking Programs with Lists. - Alain Finkel; Étienne Lozes; Arnaud Sangnier (ILC, 2007)

A Spatial Equational Logic for the Applied pi-Calculus. - Étienne Lozes; Jules Villard (CONCUR, 2008)

Separability in the Ambient Logic. - Étienne Lozes; Daniel Hirschkoff; Davide Sangiorgi (Log. Methods Comput. Sci., 2008)

Proving Copyless Message Passing. - Jules Villard; Étienne Lozes; Cristiano Calcagno (APLAS, 2009)

Beyond Shapes: Lists with Ordered Data. - Kshitij Bansal; Rémi Brochenin; Étienne Lozes (FoSSaCS, 2009)

Reasoning about sequences of memory states. - Rémi Brochenin; Stéphane Demri; Étienne Lozes (Ann. Pure Appl. Log., 2009)

Tracking Heaps That Hop with Heap-Hop. - Jules Villard; Étienne Lozes; Cristiano Calcagno (TACAS, 2010)

A spatial equational logic for the applied pi-calculus. - Étienne Lozes; Jules Villard (Distributed Comput., 2010)

Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus. - Florent Jacquemard; Étienne Lozes; Ralf Treinen; Jules Villard (TOSCA, 2011)

Reliable Contracts for Unreliable Half-Duplex Communications. - Étienne Lozes; Jules Villard (WS-FM, 2011)

Model-Checking the Higher-Dimensional Modal mu-Calculus - Martin Lange; Étienne Lozes (FICS, 2012)

Shared Contract-Obedient Endpoints - Étienne Lozes; Jules Villard (ICE, 2012)

On the almighty wand. - Rémi Brochenin; Stéphane Demri; Étienne Lozes (Inf. Comput., 2012)

Revealing vs. Concealing: More Simulation Games for Büchi Inclusion. - Milka Hutagalung; Martin Lange; Étienne Lozes (LATA, 2013)

Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic. - Martin Lange; Étienne Lozes (IFIP TCS, 2014)

Buffered Simulation Games for Büchi Automata. - Milka Hutagalung; Martin Lange; Étienne Lozes (AFL, 2014)

Model-checking process equivalences. - Martin Lange; Étienne Lozes; Manuel Vargas Guzmán 001 (Theor. Comput. Sci., 2014)

Conjunctive Visibly-Pushdown Path Queries. - Martin Lange; Étienne Lozes (FCT, 2015)

A Type-Directed Negation Elimination. - Étienne Lozes (FICS, 2015)

Shared contract-obedient channels. - Étienne Lozes; Jules Villard (Sci. Comput. Program., 2015)

Multi-Buffer Simulations for Trace Language Inclusion. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (GandALF, 2016)

Two-Buffer Simulation Games. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (Cassting/SynCoP, 2016)

On Symbolic Heaps Modulo Permission Theories. - Stéphane Demri; Étienne Lozes; Denis Lugiez (FSTTCS, 2017)

On the relationship between higher-order recursion schemes and higher-order fixpoint logic. - Naoki Kobayashi 001; Étienne Lozes; Florian Bruse (POPL, 2017)

Space-Efficient Fragments of Higher-Order Fixpoint Logic. - Florian Bruse; Martin Lange; Étienne Lozes (RP, 2017)

The Effects of Adding Reachability Predicates in Propositional Separation Logic. - Stéphane Demri; Étienne Lozes; Alessio Mansutti (FoSSaCS, 2018)

Multi-buffer simulations: Decidability and complexity. - Milka Hutagalung; Norbert Hundeshagen; Dietrich Kuske; Martin Lange; Étienne Lozes (Inf. Comput., 2018)

On the k-synchronizability for mailbox systems. - Cinzia Di Giusto; Laetitia Laversa; Étienne Lozes (CoRR, 2019)

Internal Calculi for Separation Logics. - Stéphane Demri; Étienne Lozes; Alessio Mansutti (CSL, 2020)

On the k-synchronizability of Systems. - Cinzia Di Giusto; Laetitia Laversa; Étienne Lozes (FoSSaCS, 2020)

A Unifying Framework for Deciding Synchronizability. - Benedikt Bollig; Cinzia Di Giusto; Alain Finkel; Laetitia Laversa; Étienne Lozes; Amrita Suresh 001 (CONCUR, 2021)

Towards Generalised Half-Duplex Systems. - Cinzia Di Giusto; Loïc Germerie Guizouarn; Étienne Lozes (ICE, 2021)

The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic. - Florian Bruse; Martin Lange; Étienne Lozes (Fundam. Informaticae, 2021)

A Complete Axiomatisation for Quantifier-Free Separation Logic. - Stéphane Demri; Étienne Lozes; Alessio Mansutti (Log. Methods Comput. Sci., 2021)

The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic. - Stéphane Demri; Étienne Lozes; Alessio Mansutti (ACM Trans. Comput. Log., 2021)

The Tail-Recursive Fragment of Timed Recursive CTL. - Florian Bruse; Martin Lange; Étienne Lozes (TIME, 2022)

A non-sequential hierarchy of message-passing models. - Cinzia Di Giusto; Davide Ferré; Laetitia Laversa; Étienne Lozes (CoRR, 2022)

Weakly Synchronous Systems with Three Machines Are Turing Powerful. - Cinzia Di Giusto; Davide Ferré; Étienne Lozes; Nicolas Nisse (RP, 2023)

Synchronizability of Communicating Finite State Machines is not Decidable. - Alain Finkel; Étienne Lozes (Log. Methods Comput. Sci., 2023)

A Partial Order View of Message-Passing Communication Models. - Cinzia Di Giusto; Davide Ferré; Laetitia Laversa; Étienne Lozes (Proc. ACM Program. Lang., 2023)

Multiparty half-duplex systems and synchronous communications. - Cinzia Di Giusto; Loïc Germerie Guizouarn; Étienne Lozes (J. Log. Algebraic Methods Program., 2023)

Guessing the Buffer Bound for k-Synchronizability. - Cinzia Di Giusto; Laetitia Laversa; Étienne Lozes (Int. J. Found. Comput. Sci., 2023)

Realisability and Complementability of Multiparty Session Types. - Cinzia Di Giusto; Étienne Lozes; Pascal Urso (CoRR, 2025)