53 Search Results for "Talbot, Jean-Marc"

Volume

LIPIcs, Volume 62

25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

CSL 2016, August 29 to September 1, 2016, Marseille, France

Editors: Jean-Marc Talbot and Laurent Regnier

Document
DOI: 10.4230/LIPIcs.CSL.2026.40
The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.45
Reasoning About Quality in Hyperproperties

Authors: Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman [Almagor et al., 2016] where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.
Cite as

Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning About Quality in Hyperproperties. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{graepler_et_al:LIPIcs.CSL.2026.45,
  author =	{Graepler, Samuel and Monmege, Benjamin and Talbot, Jean-Marc},
  title =	{{Reasoning About Quality in Hyperproperties}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{45:1--45:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.45},
  URN =		{urn:nbn:de:0030-drops-254704},
  doi =		{10.4230/LIPIcs.CSL.2026.45},
  annote =	{Keywords: Hyperlogics, Automata-based model checking, Quantitative verification}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.40
Symmetric Proofs in the Ideal Proof System

Authors: Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.
Cite as

Anuj Dawar, Erich Grädel, Leon Kullmann, and Benedikt Pago. Symmetric Proofs in the Ideal Proof System. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.MFCS.2025.40,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Kullmann, Leon and Pago, Benedikt},
  title =	{{Symmetric Proofs in the Ideal Proof System}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.40},
  URN =		{urn:nbn:de:0030-drops-241477},
  doi =		{10.4230/LIPIcs.MFCS.2025.40},
  annote =	{Keywords: proof complexity, algebraic complexity, descriptive complexity, symmetric circuits, graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.24
Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani and Gianluigi Zavattaro

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.
Cite as

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{padovani_et_al:LIPIcs.ECOOP.2025.24,
  author =	{Padovani, Luca and Zavattaro, Gianluigi},
  title =	{{Fair Termination of Asynchronous Binary Sessions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{24:1--24:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.24},
  URN =		{urn:nbn:de:0030-drops-233169},
  doi =		{10.4230/LIPIcs.ECOOP.2025.24},
  annote =	{Keywords: Binary sessions, fair asynchronous subtyping, fair termination, linear logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.20
Boundedness of Cost Register Automata over the Integer Min-Plus Semiring

Authors: Andrei Draghici, Radosław Piórkowski, and Andrew Ryzhikov

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Cost register automata (CRAs) are deterministic automata with registers taking values from a fixed semiring. A CRA computes a function from words to values from this semiring. CRAs are tightly related to well-studied weighted automata. Given a CRA, the boundedness problem asks if there exists a natural number N such that for every word, the value of the CRA on this word does not exceed N. This problem is known to be undecidable for the class of linear CRAs over the integer min-plus semiring (ℤ∪{+∞}, min, +), but very little is known about its subclasses. In this paper, we study boundedness of copyless linear CRAs with resets over the integer min-plus semiring. We show that it is decidable for such CRAs with at most two registers. More specifically, we show that it is, respectively, NL-complete and in coNP if the numbers in the input are presented in unary and binary. We also provide complexity results for two classes with an arbitrary number of registers. Namely, we show that for CRAs that use the minimum operation only in the output function, boundedness is PSPACE-complete if transferring values to other registers is allowed, and is coNP-complete otherwise. Finally, for each f_i in the hierarchy of fast-growing functions, we provide a stateless CRA with i registers whose output exceeds N only on runs longer than f_i(N). Our construction yields a non-elementary lower bound already for four registers.
Cite as

Andrei Draghici, Radosław Piórkowski, and Andrew Ryzhikov. Boundedness of Cost Register Automata over the Integer Min-Plus Semiring. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{draghici_et_al:LIPIcs.CSL.2025.20,
  author =	{Draghici, Andrei and Pi\'{o}rkowski, Rados{\l}aw and Ryzhikov, Andrew},
  title =	{{Boundedness of Cost Register Automata over the Integer Min-Plus Semiring}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{20:1--20:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.20},
  URN =		{urn:nbn:de:0030-drops-227775},
  doi =		{10.4230/LIPIcs.CSL.2025.20},
  annote =	{Keywords: cost register automata, boundedness, decidability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.6
Weighted Automata and Expressions over Pre-Rational Monoids

Authors: Nicolas Baudru, Louis-Marie Dando, Nathan Lhote, Benjamin Monmege, Pierre-Alain Reynier, and Jean-Marc Talbot

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature; on one hand, lifting this result to a weighted setting has been widely studied. On the other hand, beyond the free monoid, different monoids can be considered: for instance, two-way automata, and even tree-walking automata, can be described by expressions using the free inverse monoid. In the present work, we aim at combining both research directions and consider weighted extensions of automata and expressions over a class of monoids that we call pre-rational, generalising both the free inverse monoid and graded monoids. The presence of idempotent elements in these pre-rational monoids leads in the weighted setting to consider infinite sums. To handle such sums, we will have to restrict ourselves to rationally additive semirings. Our main result is thus a generalisation of the Kleene theorem for pre-rational monoids and rationally additive semirings. As a corollary, we obtain a class of expressions equivalent to weighted two-way automata, as well as one for tree-walking automata.
Cite as

Nicolas Baudru, Louis-Marie Dando, Nathan Lhote, Benjamin Monmege, Pierre-Alain Reynier, and Jean-Marc Talbot. Weighted Automata and Expressions over Pre-Rational Monoids. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{baudru_et_al:LIPIcs.CSL.2022.6,
  author =	{Baudru, Nicolas and Dando, Louis-Marie and Lhote, Nathan and Monmege, Benjamin and Reynier, Pierre-Alain and Talbot, Jean-Marc},
  title =	{{Weighted Automata and Expressions over Pre-Rational Monoids}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.6},
  URN =		{urn:nbn:de:0030-drops-157266},
  doi =		{10.4230/LIPIcs.CSL.2022.6},
  annote =	{Keywords: Weighted Automata and Expressions, Inverse Monoids, Two-Way Automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.75
Determinisation of Finitely-Ambiguous Copyless Cost Register Automata

Authors: Théodore Lopez, Benjamin Monmege, and Jean-Marc Talbot

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
Cost register automata (CRA) are machines reading an input word while computing values using write-only registers: values from registers are combined using the two operations, as well as the constants, of a semiring. Particularly interesting is the subclass of copyless CRAs where the content of a register cannot be used twice for updating the registers. Originally deterministic, non-deterministic variant of CRA may also be defined: the semantics is then obtained by combining the values of all accepting runs with the additive operation of the semiring (as for weighted automata). We show that finitely-ambiguous copyless non-deterministic CRAs (i.e. the ones that admit a bounded number of accepting runs on every input word) can be effectively transformed into an equivalent copyless (deterministic) CRA, without requiring any specific property on the semiring. As a corollary, this also shows that regular look-ahead can effectively be removed from copyless CRAs.
Cite as

Théodore Lopez, Benjamin Monmege, and Jean-Marc Talbot. Determinisation of Finitely-Ambiguous Copyless Cost Register Automata. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 75:1-75:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lopez_et_al:LIPIcs.MFCS.2019.75,
  author =	{Lopez, Th\'{e}odore and Monmege, Benjamin and Talbot, Jean-Marc},
  title =	{{Determinisation of Finitely-Ambiguous Copyless Cost Register Automata}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{75:1--75:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.75},
  URN =		{urn:nbn:de:0030-drops-110190},
  doi =		{10.4230/LIPIcs.MFCS.2019.75},
  annote =	{Keywords: Cost-register automata, Look-ahead removal, Unambiguity, Determinisation}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2016
LIPIcs, Volume 62, CSL'16, Complete Volume

Authors: Jean-Marc Talbot and Laurent Regnier

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
LIPIcs, Volume 62, CSL'16, Complete Volume
Cite as

25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Proceedings{talbot_et_al:LIPIcs.CSL.2016,
  title =	{{LIPIcs, Volume 62, CSL'16, Complete Volume}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016},
  URN =		{urn:nbn:de:0030-drops-66715},
  doi =		{10.4230/LIPIcs.CSL.2016},
  annote =	{Keywords: Conference Proceedings, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory, Languages Constructs and Features, Knowledge Representations Formalisms and Methods, Theory of Computation, Mathematical Logic}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2016.0
Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers

Authors: Jean-Marc Talbot and Laurent Regnier

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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

25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{talbot_et_al:LIPIcs.CSL.2016.0,
  author =	{Talbot, Jean-Marc and Regnier, Laurent},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.0},
  URN =		{urn:nbn:de:0030-drops-65405},
  doi =		{10.4230/LIPIcs.CSL.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization, External Reviewers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.1
The Ackermann Award 2016

Authors: Thierry Coquand and Anuj Dawar

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.
Cite as

Thierry Coquand and Anuj Dawar. The Ackermann Award 2016. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.CSL.2016.1,
  author =	{Coquand, Thierry and Dawar, Anuj},
  title =	{{The Ackermann Award 2016}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.1},
  URN =		{urn:nbn:de:0030-drops-65419},
  doi =		{10.4230/LIPIcs.CSL.2016.1},
  annote =	{Keywords: Ackermann Award, Computer Science, Logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2016.2
Infinite Domain Constraint Satisfaction Problem (Invited Talk)

Authors: Libor Barto

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The computational and descriptive complexity of finite domain fixed template constraint satisfaction problem (CSP) is a well developed topic that combines several areas in mathematics and computer science. Allowing the domain to be infinite provides a way larger playground which covers many more computational problems and requires further mathematical tools. I will talk about some of the research challenges and recent progress on them.
Cite as

Libor Barto. Infinite Domain Constraint Satisfaction Problem (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{barto:LIPIcs.CSL.2016.2,
  author =	{Barto, Libor},
  title =	{{Infinite Domain Constraint Satisfaction Problem}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.2},
  URN =		{urn:nbn:de:0030-drops-65427},
  doi =		{10.4230/LIPIcs.CSL.2016.2},
  annote =	{Keywords: Descriptive complexity, Constraint Satisfaction Problem}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2016.3
Automated Synthesis: Going Distributed (Invited Talk)

Authors: Anca Muscholl

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Synthesis is particularly challenging for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. The talk provides an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring.
Cite as

Anca Muscholl. Automated Synthesis: Going Distributed (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{muscholl:LIPIcs.CSL.2016.3,
  author =	{Muscholl, Anca},
  title =	{{Automated Synthesis: Going Distributed}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.3},
  URN =		{urn:nbn:de:0030-drops-65436},
  doi =		{10.4230/LIPIcs.CSL.2016.3},
  annote =	{Keywords: Concurrent programs, Distributed synthesis, Runtime monitoring}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2016.4
Analytic Calculi for Non-Classical Logics: Theory and Applications (Invited Talk)

Authors: Agata Ciabattoni

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The possession of a suitable proof-calculus is the starting point for many investigations into a logic, including decidability and complexity, computational interpretations and automated theorem proving. By suitable proof-calculus we mean a calculus whose proofs exhibit some notion of subformula property ("analyticity"). In this talk we describe a method for the algorithmic introduction of analytic sequent-style calculi for a wide range of non-classical logics starting from Hilbert systems. To demonstrate the widespread applicability of this method, we discuss how to use the introduced calculi for proving various results ranging from Curry-Howard isomorphism to new interpretative tools for Indology.
Cite as

Agata Ciabattoni. Analytic Calculi for Non-Classical Logics: Theory and Applications (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{ciabattoni:LIPIcs.CSL.2016.4,
  author =	{Ciabattoni, Agata},
  title =	{{Analytic Calculi for Non-Classical Logics: Theory and Applications}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.4},
  URN =		{urn:nbn:de:0030-drops-65440},
  doi =		{10.4230/LIPIcs.CSL.2016.4},
  annote =	{Keywords: Proof theory, Fuzzy logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2016.5
Coalgebraic Learning (Invited Talk)

Authors: Alexandra Silva

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The area of automata learning was pioneered by Angluin in the 80's. Her original algorithm, which applied to regular languages and deterministic automata, has been extended to various types of automata and used in software and hardware verification. In this talk, we will take an abstract perspective at automata learning. We show how the correctness of the original algorithm and many extensions can be captured in one proof using coalgebraic techniques. We also show that a novel algorithm for nominal automata can be derived from the abstract framework.
Cite as

Alexandra Silva. Coalgebraic Learning (Invited Talk). In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{silva:LIPIcs.CSL.2016.5,
  author =	{Silva, Alexandra},
  title =	{{Coalgebraic Learning}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.5},
  URN =		{urn:nbn:de:0030-drops-65455},
  doi =		{10.4230/LIPIcs.CSL.2016.5},
  annote =	{Keywords: Automata learning, coalgebraic techniques}
}
  • Refine by Type
  • 52 Document/PDF
  • 5 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 2 2026
  • 3 2025
  • 1 2022
  • 1 2019
  • 45 2016
  • Show More...

  • Refine by Author
  • 6 Talbot, Jean-Marc
  • 3 Monmege, Benjamin
  • 2 Altenkirch, Thorsten
  • 2 Baelde, David
  • 2 Dawar, Anuj
  • Show More...

  • Refine by Series/Journal
  • 51 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 2 Theory of computation → Quantitative automata
  • 1 Security and privacy
  • 1 Theory of computation → Algebraic complexity theory
  • 1 Theory of computation → Finite Model Theory
  • 1 Theory of computation → Formal languages and automata theory
  • Show More...

  • Refine by Keyword
  • 4 homotopy type theory
  • 3 computational complexity
  • 3 finite model theory
  • 3 linear logic
  • 2 Constraint Satisfaction Problem
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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