96 Search Results for "Pagès, Gilles"

Document
DOI: 10.4230/LIPIcs.CP.2023.6
Optimization of Short-Term Underground Mine Planning Using Constraint Programming

Authors: Younes Aalian, Gilles Pesant, and Michel Gamache

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
Short-term underground mine planning problems are often difficult to solve due to the large number of activities and diverse machine types to be scheduled, as well as multiple operational constraints. This paper presents a Constraint Programming (CP) model to optimize short-term scheduling for the Meliadine underground gold mine in Nunavut, Canada, taking into consideration operational constraints and the daily development and production targets of the mine plan. To evaluate the efficacy of the developed CP short-term planning model, we compare schedules generated by the CP model with the ones created manually by the mine planner for two real data sets. Results demonstrate that the CP model outperforms the manual approach by generating more efficient schedules with lower makespans.
Cite as

Younes Aalian, Gilles Pesant, and Michel Gamache. Optimization of Short-Term Underground Mine Planning Using Constraint Programming. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{aalian_et_al:LIPIcs.CP.2023.6,
  author =	{Aalian, Younes and Pesant, Gilles and Gamache, Michel},
  title =	{{Optimization of Short-Term Underground Mine Planning Using Constraint Programming}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.6},
  URN =		{urn:nbn:de:0030-drops-190430},
  doi =		{10.4230/LIPIcs.CP.2023.6},
  annote =	{Keywords: Mine planning, Constraint Programming, Short-term planning, Underground mine, Scheduling}
}
Document
DOI: 10.4230/LIPIcs.CP.2023.9
Guiding Backtrack Search by Tracking Variables During Constraint Propagation

Authors: Gilles Audemard, Christophe Lecoutre, and Charles Prud'homme

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
It is well-known that variable ordering heuristics play a central role in solving efficiently Constraint Satisfaction Problem (CSP) instances. From the early 80’s, and during more than two decades, the dynamic variable ordering heuristic selecting the variable with the smallest domain was clearly prevailing. Then, from the mid 2000’s, some adaptive heuristics have been introduced: their principle is to collect some useful information during the search process in order to take better informed decisions. Among those adaptive heuristics, wdeg/dom (and its variants) remains particularly robust. In this paper, we introduce an original heuristic based on the midway processing of failing executions of constraint propagation: this heuristic called pick/dom tracks the variables that are directly involved in the process of constraint propagation, when ending with a conflict. The robustness of this new heuristic is demonstrated from a large experimentation conducted with the constraint solver ACE. Interestingly enough, one can observe some complementary between the early, midway and late forms of processing of conflicts.
Cite as

Gilles Audemard, Christophe Lecoutre, and Charles Prud'homme. Guiding Backtrack Search by Tracking Variables During Constraint Propagation. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{audemard_et_al:LIPIcs.CP.2023.9,
  author =	{Audemard, Gilles and Lecoutre, Christophe and Prud'homme, Charles},
  title =	{{Guiding Backtrack Search by Tracking Variables During Constraint Propagation}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.9},
  URN =		{urn:nbn:de:0030-drops-190461},
  doi =		{10.4230/LIPIcs.CP.2023.9},
  annote =	{Keywords: Variable Ordering Heuristics, Variable Weighting}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.4
Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory

Authors: Emilie Grienenberger

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Systems in which classical and intuitionistic logics coexist are called ecumenical. Such a system allows for interoperability and hybridization between classical and constructive propositions and proofs. We study Ecumenical STT, a theory expressed in the logical framework of the λΠ-calculus modulo theory. We prove soudness and conservativity of four subtheories of Ecumenical STT with respect to constructive and classical predicate logic and simple type theory. We also prove the weak normalization of well-typed terms and thus the consistency of Ecumenical STT.
Cite as

Emilie Grienenberger. Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{grienenberger:LIPIcs.TYPES.2022.4,
  author =	{Grienenberger, Emilie},
  title =	{{Expressing Ecumenical Systems in the \lambda\Pi-Calculus Modulo Theory}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.4},
  URN =		{urn:nbn:de:0030-drops-184479},
  doi =		{10.4230/LIPIcs.TYPES.2022.4},
  annote =	{Keywords: dependent types, predicate logic, higher order logic, constructivism, interoperability, ecumenical logics}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.18
On the Origins of Coccinelle

Authors: Julia Lawall

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Coccinelle is a program-transformation system for C code. It has been under development since 2005 and has been extensively used on the Linux kernel. The design of Coccinelle was inspired in part by the author’s previous experience in using Stratego/XT, developed by Eelco Visser. This paper reflects on some of Coccinelle’s design choices and their relation to Eelco Visser’s work.
Cite as

Julia Lawall. On the Origins of Coccinelle. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 18:1-18:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{lawall:OASIcs.EVCS.2023.18,
  author =	{Lawall, Julia},
  title =	{{On the Origins of Coccinelle}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{18:1--18:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.18},
  URN =		{urn:nbn:de:0030-drops-177884},
  doi =		{10.4230/OASIcs.EVCS.2023.18},
  annote =	{Keywords: Linux kernel, Coccinelle, Stratego/XT, program transformation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.19
Translating Proofs from an Impredicative Type System to a Predicative One

Authors: Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way. In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases. During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones. The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.
Cite as

Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19,
  author =	{Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar},
  title =	{{Translating Proofs from an Impredicative Type System to a Predicative One}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19},
  URN =		{urn:nbn:de:0030-drops-174801},
  doi =		{10.4230/LIPIcs.CSL.2023.19},
  annote =	{Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.13
Simulations for Event-Clock Automata

Authors: S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations. In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.
Cite as

S. Akshay, Paul Gastin, R. Govind, and B. Srivathsan. Simulations for Event-Clock Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{akshay_et_al:LIPIcs.CONCUR.2022.13,
  author =	{Akshay, S. and Gastin, Paul and Govind, R. and Srivathsan, B.},
  title =	{{Simulations for Event-Clock Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.13},
  URN =		{urn:nbn:de:0030-drops-170766},
  doi =		{10.4230/LIPIcs.CONCUR.2022.13},
  annote =	{Keywords: Event-clock automata, verification, zones, simulations, reachability}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.28
A New Exact Solver for (Weighted) Max#SAT

Authors: Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.
Cite as

Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{audemard_et_al:LIPIcs.SAT.2022.28,
  author =	{Audemard, Gilles and Lagniez, Jean-Marie and Miceli, Marie},
  title =	{{A New Exact Solver for (Weighted) Max#SAT}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.28},
  URN =		{urn:nbn:de:0030-drops-167022},
  doi =		{10.4230/LIPIcs.SAT.2022.28},
  annote =	{Keywords: Max#SAT, EMaj-SAT, Weighted Projected Model Counting, SSAT}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.30
Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints

Authors: Daphné Lafleur, Sarath Chandar, and Gilles Pesant

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
While Machine Learning (ML) techniques are good at generating data similar to a dataset, they lack the capacity to enforce constraints. On the other hand, any solution to a Constraint Programming (CP) model satisfies its constraints but has no obligation to imitate a dataset. Yet, we sometimes need both. In this paper we borrow RL-Tuner, a Reinforcement Learning (RL) algorithm introduced to tune neural networks, as our enabling architecture to exploit the respective strengths of ML and CP. RL-Tuner maximizes the sum of a pretrained network’s learned probabilities and of manually-tuned penalties for each violated constraint. We replace the latter with outputs of a CP model representing the marginal probabilities of each value and the number of constraint violations. As was the case for the original RL-Tuner, we apply our algorithm to music generation since it is a highly-constrained domain for which CP is especially suited. We show that combining ML and CP, as opposed to using them individually, allows the agent to reflect the pretrained network while taking into account constraints, leading to melodic lines that respect both the corpus' style and the music theory constraints.
Cite as

Daphné Lafleur, Sarath Chandar, and Gilles Pesant. Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lafleur_et_al:LIPIcs.CP.2022.30,
  author =	{Lafleur, Daphn\'{e} and Chandar, Sarath and Pesant, Gilles},
  title =	{{Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.30},
  URN =		{urn:nbn:de:0030-drops-166594},
  doi =		{10.4230/LIPIcs.CP.2022.30},
  annote =	{Keywords: Constraint programming, reinforcement learning, RNN, music generation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.21
Linear Lambda-Calculus is Linear

Authors: Alejandro Díaz-Caro and Gilles Dowek

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.
Cite as

Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{diazcaro_et_al:LIPIcs.FSCD.2022.21,
  author =	{D{\'\i}az-Caro, Alejandro and Dowek, Gilles},
  title =	{{Linear Lambda-Calculus is Linear}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.21},
  URN =		{urn:nbn:de:0030-drops-163024},
  doi =		{10.4230/LIPIcs.FSCD.2022.21},
  annote =	{Keywords: Proof theory, Lambda calculus, Linear logic, Quantum computing}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.25
Adequate and Computational Encodings in the Logical Framework Dedukti

Authors: Thiago Felicissimo

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem - i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational - that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.
Cite as

Thiago Felicissimo. Adequate and Computational Encodings in the Logical Framework Dedukti. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{felicissimo:LIPIcs.FSCD.2022.25,
  author =	{Felicissimo, Thiago},
  title =	{{Adequate and Computational Encodings in the Logical Framework Dedukti}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.25},
  URN =		{urn:nbn:de:0030-drops-163064},
  doi =		{10.4230/LIPIcs.FSCD.2022.25},
  annote =	{Keywords: Type Theory, Logical Frameworks, Rewriting, Dedukti, Pure Type Systems}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2022.18
Asymptotic Bounds on the Combinatorial Diameter of Random Polytopes

Authors: Gilles Bonnet, Daniel Dadush, Uri Grupel, Sophie Huiberts, and Galyna Livshyts

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
The combinatorial diameter diam(P) of a polytope P is the maximum shortest path distance between any pair of vertices. In this paper, we provide upper and lower bounds on the combinatorial diameter of a random "spherical" polytope, which is tight to within one factor of dimension when the number of inequalities is large compared to the dimension. More precisely, for an n-dimensional polytope P defined by the intersection of m i.i.d. half-spaces whose normals are chosen uniformly from the sphere, we show that diam(P) is Ω(n m^{1/(n-1)}) and O(n² m^{1/(n-1)} + n⁵ 4ⁿ) with high probability when m ≥ 2^{Ω(n)}. For the upper bound, we first prove that the number of vertices in any fixed two dimensional projection sharply concentrates around its expectation when m is large, where we rely on the Θ(n² m^{1/(n-1)}) bound on the expectation due to Borgwardt [Math. Oper. Res., 1999]. To obtain the diameter upper bound, we stitch these "shadows paths" together over a suitable net using worst-case diameter bounds to connect vertices to the nearest shadow. For the lower bound, we first reduce to lower bounding the diameter of the dual polytope P^∘, corresponding to a random convex hull, by showing the relation diam(P) ≥ (n-1)(diam(P^∘)-2). We then prove that the shortest path between any "nearly" antipodal pair vertices of P^∘ has length Ω(m^{1/(n-1)}).
Cite as

Gilles Bonnet, Daniel Dadush, Uri Grupel, Sophie Huiberts, and Galyna Livshyts. Asymptotic Bounds on the Combinatorial Diameter of Random Polytopes. In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.SoCG.2022.18,
  author =	{Bonnet, Gilles and Dadush, Daniel and Grupel, Uri and Huiberts, Sophie and Livshyts, Galyna},
  title =	{{Asymptotic Bounds on the Combinatorial Diameter of Random Polytopes}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{18:1--18:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.18},
  URN =		{urn:nbn:de:0030-drops-160269},
  doi =		{10.4230/LIPIcs.SoCG.2022.18},
  annote =	{Keywords: Random Polytopes, Combinatorial Diameter, Hirsch Conjecture}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2022.1
Local Limit of Random Discrete Surface with (Or Without!) a Statistical Physics Model (Invited Talk)

Authors: Marie Albenque

Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)

Abstract
A planar map is an embedding of a planar graph in the sphere, considered up to deformations. A triangulation is a planar map, where all the faces are triangles. In 2003, in order to define a model of generic planar geometry, Angel and Schramm studied the limit of random triangulations on the sphere, [Angel and Schramm, 2003]. They proved that this model of random maps converges for the Benjamini-Schramm topology (see [Benjamini and Schramm, 2001]), or local topology, towards the now famous Uniform Infinite Planar Triangulation (or UIPT), a probability distribution on infinite triangulations, see Figure 1. Soon after, Angel [Angel, 2003] studied some properties of the UIPT. He established that the volume of the balls the UIPT of radius R scales as R⁴. Similar results (but with quite different proofs) were then obtained for quadrangulations by Chassaing and Durhuus and Krikun. The results cited above deal with models of maps that fall in the same "universality class", identified in the physics literature as the class of "pure 2D quantum gravity": the generating series all admit the same critical exponent and the volume of the balls of the local limits of several of those models of random maps are known to grow as R⁴. To capture this universal behaviour, a good framework is to consider scaling limits of random maps in the Gromov Hausdorff topology. Indeed, for a wide variety of models the scaling limit exists and is the so-called Brownian map [Le Gall, 2013; Miermont, 2013], see Figure 2. To escape this pure gravity behaviour, physicists have long ago understood that one should "couple gravity with matter", that is, consider models of random maps endowed with a statistical physics model. I will present in particular the case of triangulations decorated by an Ising model. It consists in colouring in black and white the vertices of a triangulation, and consider probability distribution which are now biased by their number of monochromatic edges. In a recent work, in collaboration with Laurent Ménard and Gilles Schaeffer [Albenque et al., 2020], we proved that the local limit of this model also exists. In this talk, I will present these results and explain the main ideas underlying their proof, which rely in part on some enumerative formulas obtained by Tutte in the 60s [Tutte, 1962], or their generalization to coloured triangulations by Bernardi and Bousquet-Mélou [Bernardi and Bousquet-Mélou, 2011].
Cite as

Marie Albenque. Local Limit of Random Discrete Surface with (Or Without!) a Statistical Physics Model (Invited Talk). In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{albenque:LIPIcs.STACS.2022.1,
  author =	{Albenque, Marie},
  title =	{{Local Limit of Random Discrete Surface with (Or Without!) a Statistical Physics Model}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.1},
  URN =		{urn:nbn:de:0030-drops-158118},
  doi =		{10.4230/LIPIcs.STACS.2022.1},
  annote =	{Keywords: Random graphs, triangulations, Benjamini-Schramm convergence, Ising model}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.18
An Interval Constraint Programming Approach for Quasi Capture Tube Validation

Authors: Abderahmane Bedouhene, Bertrand Neveu, Gilles Trombettoni, Luc Jaulin, and Stéphane Le Menec

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

Abstract
Proving that the state of a controlled nonlinear system always stays inside a time moving bubble (or capture tube) amounts to proving the inconsistency of a set of nonlinear inequalities in the time-state space. In practice however, even with a good intuition, it is difficult for a human to find such a capture tube except for simple examples. In 2014, Jaulin et al. established properties that support a new interval approach for validating a quasi capture tube, i.e. a candidate tube (with a simple form) from which the mobile system can escape, but into which it enters again before a given time. A quasi capture tube is easy to find in practice for a controlled system. Merging the trajectories originated from the candidate tube yields the smallest capture tube enclosing it. This paper proposes an interval constraint programming solver dedicated to the quasi capture tube validation. The problem is viewed as a differential CSP where the functional variables correspond to the state variables of the system and the constraints define system trajectories that escape from the candidate tube "for ever". The solver performs a branch and contract procedure for computing the trajectories that escape from the candidate tube. If no solution is found, the quasi capture tube is validated and, as a side effect, a corrected smallest capture tube enclosing the quasi one is computed. The approach is experimentally validated on several examples having 2 to 5 degrees of freedom.
Cite as

Abderahmane Bedouhene, Bertrand Neveu, Gilles Trombettoni, Luc Jaulin, and Stéphane Le Menec. An Interval Constraint Programming Approach for Quasi Capture Tube Validation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bedouhene_et_al:LIPIcs.CP.2021.18,
  author =	{Bedouhene, Abderahmane and Neveu, Bertrand and Trombettoni, Gilles and Jaulin, Luc and Le Menec, St\'{e}phane},
  title =	{{An Interval Constraint Programming Approach for Quasi Capture Tube Validation}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{18:1--18:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.18},
  URN =		{urn:nbn:de:0030-drops-153093},
  doi =		{10.4230/LIPIcs.CP.2021.18},
  annote =	{Keywords: Constraint satisfaction problem, Interval analysis, Dynamical systems, Contractor}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.LDK.2021
OASIcs, Volume 93, LDK 2021, Complete Volume

Authors: Dagmar Gromann, Gilles Sérasset, Thierry Declerck, John P. McCrae, Jorge Gracia, Julia Bosque-Gil, Fernando Bobillo, and Barbara Heinisch

Published in: OASIcs, Volume 93, 3rd Conference on Language, Data and Knowledge (LDK 2021)

Abstract
OASIcs, Volume 93, LDK 2021, Complete Volume
Cite as

3rd Conference on Language, Data and Knowledge (LDK 2021). Open Access Series in Informatics (OASIcs), Volume 93, pp. 1-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{gromann_et_al:OASIcs.LDK.2021,
  title =	{{OASIcs, Volume 93, LDK 2021, Complete Volume}},
  booktitle =	{3rd Conference on Language, Data and Knowledge (LDK 2021)},
  pages =	{1--516},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-199-3},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{93},
  editor =	{Gromann, Dagmar and S\'{e}rasset, Gilles and Declerck, Thierry and McCrae, John P. and Gracia, Jorge and Bosque-Gil, Julia and Bobillo, Fernando and Heinisch, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.LDK.2021},
  URN =		{urn:nbn:de:0030-drops-145352},
  doi =		{10.4230/OASIcs.LDK.2021},
  annote =	{Keywords: OASIcs, Volume 93, LDK 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.LDK.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Dagmar Gromann, Gilles Sérasset, Thierry Declerck, John P. McCrae, Jorge Gracia, Julia Bosque-Gil, Fernando Bobillo, and Barbara Heinisch

Published in: OASIcs, Volume 93, 3rd Conference on Language, Data and Knowledge (LDK 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

3rd Conference on Language, Data and Knowledge (LDK 2021). Open Access Series in Informatics (OASIcs), Volume 93, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{gromann_et_al:OASIcs.LDK.2021.0,
  author =	{Gromann, Dagmar and S\'{e}rasset, Gilles and Declerck, Thierry and McCrae, John P. and Gracia, Jorge and Bosque-Gil, Julia and Bobillo, Fernando and Heinisch, Barbara},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{3rd Conference on Language, Data and Knowledge (LDK 2021)},
  pages =	{0:i--0:xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-199-3},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{93},
  editor =	{Gromann, Dagmar and S\'{e}rasset, Gilles and Declerck, Thierry and McCrae, John P. and Gracia, Jorge and Bosque-Gil, Julia and Bobillo, Fernando and Heinisch, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.LDK.2021.0},
  URN =		{urn:nbn:de:0030-drops-145364},
  doi =		{10.4230/OASIcs.LDK.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
  • Refine by Author
  • 9 Barthe, Gilles
  • 8 Geeraerts, Gilles
  • 5 Brihaye, Thomas
  • 5 Dowek, Gilles
  • 5 Monmege, Benjamin
  • Show More...

  • Refine by Classification
  • 11 Computing methodologies → Language resources
  • 9 Computing methodologies → Information extraction
  • 8 Computing methodologies → Natural language processing
  • 6 Computing methodologies → Knowledge representation and reasoning
  • 6 Computing methodologies → Lexical semantics
  • Show More...

  • Refine by Keyword
  • 4 Knowledge Graph
  • 4 NLP
  • 3 Annotation
  • 3 Dedukti
  • 3 Digital Humanities
  • Show More...

  • Refine by Type
  • 96 document

  • Refine by Publication Year
  • 49 2021
  • 7 2017
  • 7 2022
  • 6 2019
  • 5 2015
  • 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact