5 Search Results for "Thierry-Mieg, Nicolas"

Document
DOI: 10.4230/LIPIcs.SAT.2024.15
Antichain with SAT and Tries

Authors: Lukáš Holík and Pavol Vargovčík

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
We introduce a SAT-enabled version of an antichain algorithm for checking language emptiness of alternating finite automata (AFA) with complex transition relations encoded as compact logical formulae. The SAT solver is used to compute predecessors of AFA configurations, and at the same time, to evaluate the subsumption of newly found configurations in the antichain of the previously found ones. The algorithm could be naively implemented by an incremental SAT solver where the growing antichain is represented by adding new clauses. To make it efficient, we 1) force the SAT solver to prioritize largest/subsumption-strongest predecessors (so that weaker configurations are not even generated), and 2) store the antichain clauses in a special variant of a trie that allows fast subsumption testing. The experimental results suggest that the resulting emptiness checker is very efficient compared to the state of the art and that our techniques improve the performance of the SAT solver.
Cite as

Lukáš Holík and Pavol Vargovčík. Antichain with SAT and Tries. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{holik_et_al:LIPIcs.SAT.2024.15,
  author =	{Hol{\'\i}k, Luk\'{a}\v{s} and Vargov\v{c}{\'\i}k, Pavol},
  title =	{{Antichain with SAT and Tries}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{15:1--15:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.15},
  URN =		{urn:nbn:de:0030-drops-205372},
  doi =		{10.4230/LIPIcs.SAT.2024.15},
  annote =	{Keywords: SAT, Trie, Antichain, Alternating automata, Subset query}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.5
The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.
Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.25
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
Document
DOI: 10.4230/DagSemProc.09311.3
Quantum key distribution and cryptography: a survey

Authors: Romain Alléaume, Norbert Lütkenhaus, Renato Renner, Philippe Grangier, Thierry Debuisschert, Gregoire Ribordy, Nicolas Gisin, Philippe Painchault, Thomas Pornin, Louis Slavail, Michel Riguidel, Andrew Shilds, Thomas Länger, Momtchil Peev, Mehrdad Dianati, Anthony Leverrier, Andreas Poppe, Jan Bouda, Cyril Branciard, Mark Godfrey, John Rarity, Harald Weinfurter, Anton Zeilinger, and Christian Monyk

Published in: Dagstuhl Seminar Proceedings, Volume 9311, Classical and Quantum Information Assurance Foundations and Practice (2010)

Abstract
I will try to partially answer, based on a review on recent work, the following question: Can QKD and more generally quantum information be useful to cover some practical security requirements in current (and future) IT infrastructures ? I will in particular cover the following topics - practical performances of QKD - QKD network deployment - SECOQC project - Capabilities of QKD as a cryptographic primitive - comparative advantage with other solution, in order to cover practical security requirements - Quantum information and Side-channels - QKD security assurance - Thoughts about "real" Post-Quantum Cryptography
Cite as

Romain Alléaume, Norbert Lütkenhaus, Renato Renner, Philippe Grangier, Thierry Debuisschert, Gregoire Ribordy, Nicolas Gisin, Philippe Painchault, Thomas Pornin, Louis Slavail, Michel Riguidel, Andrew Shilds, Thomas Länger, Momtchil Peev, Mehrdad Dianati, Anthony Leverrier, Andreas Poppe, Jan Bouda, Cyril Branciard, Mark Godfrey, John Rarity, Harald Weinfurter, Anton Zeilinger, and Christian Monyk. Quantum key distribution and cryptography: a survey. In Classical and Quantum Information Assurance Foundations and Practice. Dagstuhl Seminar Proceedings, Volume 9311, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{alleaume_et_al:DagSemProc.09311.3,
  author =	{All\'{e}aume, Romain and L\"{u}tkenhaus, Norbert and Renner, Renato and Grangier, Philippe and Debuisschert, Thierry and Ribordy, Gregoire and Gisin, Nicolas and Painchault, Philippe and Pornin, Thomas and Slavail, Louis and Riguidel, Michel and Shilds, Andrew and L\"{a}nger, Thomas and Peev, Momtchil and Dianati, Mehrdad and Leverrier, Anthony and Poppe, Andreas and Bouda, Jan and Branciard, Cyril and Godfrey, Mark and Rarity, John and Weinfurter, Harald and Zeilinger, Anton and Monyk, Christian},
  title =	{{Quantum key distribution and cryptography: a survey}},
  booktitle =	{Classical and Quantum Information Assurance Foundations and Practice},
  pages =	{1--29},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9311},
  editor =	{Samual L. Braunstein and Hoi-Kwong Lo and Kenny Paterson and Peter Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09311.3},
  URN =		{urn:nbn:de:0030-drops-23618},
  doi =		{10.4230/DagSemProc.09311.3},
  annote =	{Keywords: QKD, QKD networks, Security assurance, Post-Quantum Cryptography}
}
Document
DOI: 10.4230/DagSemProc.08301.1
08301 Final Report – Group Testing in the Life Sciences

Authors: Alexander Schliep, Nicolas Thierry-Mieg, and Amin Shokrollahi

Published in: Dagstuhl Seminar Proceedings, Volume 8301, Group Testing in the Life Sciences (2008)

Abstract
Group testing AKA smart-pooling is a general strategy for minimizing the number of tests necessary for identifying positives among a large collection of items. It has the potential to efficiently identify and correct for experimental errors (false–positives and false–negatives). It can be used whenever tests can detect the presence of a positive in a group (or pool) of items, provided that positives are rare. Group testing has numerous applications in the life sciences, such as physical mapping, interactome mapping, drug–resistance screening, or designing DNA-microarrays, and many connections to computer science, mathematics and communications, from error-correcting codes to combinatorial design theory and to statistics. The seminar brought together researchers representing the different communities working on group testing and experimentalists from the life sciences. The desired outcome of the seminar was a better understanding of the requirements for and the possibilities of group testing in the life sciences.
Cite as

Alexander Schliep, Nicolas Thierry-Mieg, and Amin Shokrollahi. 08301 Final Report – Group Testing in the Life Sciences. In Group Testing in the Life Sciences. Dagstuhl Seminar Proceedings, Volume 8301, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{schliep_et_al:DagSemProc.08301.1,
  author =	{Schliep, Alexander and Thierry-Mieg, Nicolas and Shokrollahi, Amin},
  title =	{{08301 Final Report – Group Testing in the Life Sciences}},
  booktitle =	{Group Testing in the Life Sciences},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8301},
  editor =	{Alexander Schliep and Amin Shokrollahi and Nicolas Thierry-Mieg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08301.1},
  URN =		{urn:nbn:de:0030-drops-17806},
  doi =		{10.4230/DagSemProc.08301.1},
  annote =	{Keywords: Group Testing, Pooling, Combinatorics, Design Theory, Error correcting}
}
  • Refine by Author
  • 1 Alléaume, Romain
  • 1 Bouda, Jan
  • 1 Branciard, Cyril
  • 1 Debuisschert, Thierry
  • 1 Dianati, Mehrdad
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Alternating automata
  • 1 Antichain
  • 1 Combinatorics
  • 1 Design Theory
  • 1 Error correcting
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2024
  • 1 2008
  • 1 2010
  • 1 2019

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 About DROPS Imprint Privacy Contact