6 Search Results for "Laurent, Olivier"

Document
DOI: 10.4230/LIPIcs.FSCD.2023.26
Type Isomorphisms for Multiplicative-Additive Linear Logic

Authors: Rémi Di Guardia and Olivier Laurent

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for ⋆-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [Vincent Balat and Roberto Di Cosmo, 1999]. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [Dominic Hughes and Rob van Glabbeek, 2005]. We then use the sequent calculus to extend our results to full MALL (including all units).
Cite as

Rémi Di Guardia and Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 26:1-26:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{diguardia_et_al:LIPIcs.FSCD.2023.26,
  author =	{Di Guardia, R\'{e}mi and Laurent, Olivier},
  title =	{{Type Isomorphisms for Multiplicative-Additive Linear Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{26:1--26:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.26},
  URN =		{urn:nbn:de:0030-drops-180103},
  doi =		{10.4230/LIPIcs.FSCD.2023.26},
  annote =	{Keywords: Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.45
Solving the Non-Crossing MAPF with CP

Authors: Xiao Peng, Christine Solnon, and Olivier Simonin

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
We introduce a new Multi-Agent Path Finding (MAPF) problem which is motivated by an industrial application. Given a fleet of robots that move on a workspace that may contain static obstacles, we must find paths from their current positions to a set of destinations, and the goal is to minimise the length of the longest path. The originality of our problem comes from the fact that each robot is attached with a cable to an anchor point, and that robots are not able to cross these cables. We formally define the Non-Crossing MAPF (NC-MAPF) problem and show how to compute lower and upper bounds by solving well known assignment problems. We introduce a Variable Neighbourhood Search (VNS) approach for improving the upper bound, and a Constraint Programming (CP) model for solving the problem to optimality. We experimentally evaluate these approaches on randomly generated instances.
Cite as

Xiao Peng, Christine Solnon, and Olivier Simonin. Solving the Non-Crossing MAPF with CP. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 45:1-45:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{peng_et_al:LIPIcs.CP.2021.45,
  author =	{Peng, Xiao and Solnon, Christine and Simonin, Olivier},
  title =	{{Solving the Non-Crossing MAPF with CP}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{45:1--45:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.45},
  URN =		{urn:nbn:de:0030-drops-153367},
  doi =		{10.4230/LIPIcs.CP.2021.45},
  annote =	{Keywords: Constraint Programming (CP), Multi-Agent Path Finding (MAPF), Assignment Problems}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2020.4
Strong Bisimulation for Control Operators (Invited Talk)

Authors: Delia Kesner, Eduardo Bonelli, and Andrés Viso

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i.e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.
Cite as

Delia Kesner, Eduardo Bonelli, and Andrés Viso. Strong Bisimulation for Control Operators (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 4:1-4:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.CSL.2020.4,
  author =	{Kesner, Delia and Bonelli, Eduardo and Viso, Andr\'{e}s},
  title =	{{Strong Bisimulation for Control Operators}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.4},
  URN =		{urn:nbn:de:0030-drops-116473},
  doi =		{10.4230/LIPIcs.CSL.2020.4},
  annote =	{Keywords: Lambda-mu calculus, proof-nets, strong bisimulation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.25
Focusing in Orthologic

Authors: Olivier Laurent

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a very simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add constraints on proofs and thus to facilitate proof search. We demonstrate how to take benefits from the new systems in automatic proof search for orthologic.
Cite as

Olivier Laurent. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 25:1-25:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{laurent:LIPIcs.FSCD.2016.25,
  author =	{Laurent, Olivier},
  title =	{{Focusing in Orthologic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.25},
  URN =		{urn:nbn:de:0030-drops-59805},
  doi =		{10.4230/LIPIcs.FSCD.2016.25},
  annote =	{Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination}
}
Document
DOI: 10.4230/LITES-v002-i002-a001
From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation

Authors: Thomas Carle, Dumitru Potop-Butucaru, Yves Sorel, and David Lesens

Published in: LITES, Volume 2, Issue 2 (2015). Leibniz Transactions on Embedded Systems, Volume 2, Issue 2

Abstract
Our objective is to facilitate the development of complex time-triggered systems by automating the allocation and scheduling steps. We show that full automation is possible while taking into account the elements of complexity needed by a complex embedded control system. More precisely, we consider deterministic functional specifications provided (as often in an industrial setting) by means of synchronous data-flow models with multiple modes and multiple relative periods. We first extend this functional model with an original real-time characterization that takes advantage of our time-triggered framework to provide a simpler representation of complex end-to-end flow requirements. We also extend our specifications with additional non-functional properties specifying partitioning, allocation, and preemptability constraints. Then, we provide novel algorithms for the off-line scheduling of these extended specifications onto partitioned time-triggered architectures à la ARINC 653. The main originality of our work is that it takes into account at the same time multiple complexity elements: various types of non-functional properties (real-time, partitioning, allocation, preemptability) and functional specifications with conditional execution and multiple modes. Allocation of time slots/windows to partitions can be fully or partially provided, or synthesized by our tool. Our algorithms allow the automatic allocation and scheduling onto multi-processor (distributed) systems with a global time base, taking into account communication costs. We demonstrate our technique on a model of space flight software system with strong real-time determinism requirements.
Cite as

Thomas Carle, Dumitru Potop-Butucaru, Yves Sorel, and David Lesens. From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation. In LITES, Volume 2, Issue 2 (2015). Leibniz Transactions on Embedded Systems, Volume 2, Issue 2, pp. 01:1-01:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{carle_et_al:LITES-v002-i002-a001,
  author =	{Carle, Thomas and Potop-Butucaru, Dumitru and Sorel, Yves and Lesens, David},
  title =	{{From Dataflow Specification to Multiprocessor Partitioned Time-triggered Real-time Implementation}},
  booktitle =	{LITES, Volume 2, Issue 2 (2015)},
  pages =	{01:1--01:30},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2015},
  volume =	{2},
  number =	{2},
  editor =	{Carle, Thomas and Potop-Butucaru, Dumitru and Sorel, Yves and Lesens, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v002-i002-a001},
  doi =		{10.4230/LITES-v002-i002-a001},
  annote =	{Keywords: Time-triggered, Off-line real-time scheduling, Temporal partitioning}
}
Document
DOI: 10.4230/LITES-v001-i001-a002
TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox

Authors: Claude Helmstetter

Published in: LITES, Volume 1, Issue 1 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 1

Abstract
SystemC/TLM models, which are C++ programs, allow the simulation of embedded software before hardware low-level descriptions are available and are used as golden models for hardware verification. The verification of the SystemC/TLM models is an important issue since an error in the model can mislead the system designers or reveal an error in the specifications. An open-source simulator for SystemC/TLM is provided but there are no tools for formal verification.In order to apply model checking to a SystemC/TLM model, a semantics for standard C++ code and for specific SystemC/TLM features must be provided. The usual approach relies on the translation of the SystemC/TLM code into a formal language for which a model checker is available.We propose another approach that suppresses the error-prone translation effort. Given a SystemC/TLM program, the transitions are obtained by executing the original code using g++ and an extended SystemC library, and we ask the user to provide additional functions to store the current model state. These additional functions generally represent less than 20% of the size of the original model, and allow it to apply all CADP verification tools to the SystemC/TLM model itself.
Cite as

Claude Helmstetter. TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox. In LITES, Volume 1, Issue 1 (2014). Leibniz Transactions on Embedded Systems, Volume 1, Issue 1, pp. 02:1-02:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{helmstetter:LITES-v001-i001-a002,
  author =	{Helmstetter, Claude},
  title =	{{TLM.open: a SystemC/TLM Frontend for the CADP Verification Toolbox}},
  booktitle =	{LITES, Volume 1, Issue 1 (2014)},
  pages =	{02:1--02:18},
  journal =	{Leibniz Transactions on Embedded Systems},
  ISSN =	{2199-2002},
  year =	{2014},
  volume =	{1},
  number =	{1},
  editor =	{Helmstetter, Claude},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v001-i001-a002},
  doi =		{10.4230/LITES-v001-i001-a002},
  annote =	{Keywords: Model checking, Verification, Simulation, SystemC, Transactional modeling}
}
  • Refine by Author
  • 2 Laurent, Olivier
  • 1 Bonelli, Eduardo
  • 1 Carle, Thomas
  • 1 Di Guardia, Rémi
  • 1 Helmstetter, Claude
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Linear logic
  • 1 Computer systems organization
  • 1 Computer systems organization → Real-time systems
  • 1 Computing methodologies
  • 1 Hardware
  • Show More...

  • Refine by Keyword
  • 1 Assignment Problems
  • 1 Constraint Programming (CP)
  • 1 Lambda-mu calculus
  • 1 Linear Logic
  • 1 Model checking
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 1 2014
  • 1 2015
  • 1 2016
  • 1 2020
  • 1 2021
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact