Search Results

Documents authored by Aiguier, Marc

Document
DOI: 10.4230/LIPIcs.FSCD.2026.33
Investigations on Higher-Order Infinitary Logic

Authors: Thomas Traversié, Olivier Hermant, and Marc Aiguier

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract
Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunctions and infinite disjunctions. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr’s theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.
Cite as

Thomas Traversié, Olivier Hermant, and Marc Aiguier. Investigations on Higher-Order Infinitary Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{traversie_et_al:LIPIcs.FSCD.2026.33,
  author =	{Traversi\'{e}, Thomas and Hermant, Olivier and Aiguier, Marc},
  title =	{{Investigations on Higher-Order Infinitary Logic}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{33:1--33:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.33},
  URN =		{urn:nbn:de:0030-drops-263835},
  doi =		{10.4230/LIPIcs.FSCD.2026.33},
  annote =	{Keywords: Infinitary logic, higher-order logic, cut elimination, constructivization}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.132
Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces

Authors: Alexandre Goy, Daniela Petrişan, and Marc Aiguier

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
The powerset monad on the category of sets does not distribute over itself. Nevertheless a weaker form of distributive law of the powerset monad over itself exists and it essentially stems from the canonical Egli-Milner extension of the powerset to the category of relations. On the other hand, any regular category yields a category of relations, and some regular categories also possess a powerset-like monad, as is the Vietoris monad on compact Hausdorff spaces. We derive the Egli-Milner extension in three different frameworks : sets, toposes, and compact Hausdorff spaces. We prove that it corresponds to a monotone weak distributive law in each case by showing that the multiplication extends to relations but the unit does not. We provide an application to coalgebraic determinization of alternating automata.
Cite as

Alexandre Goy, Daniela Petrişan, and Marc Aiguier. Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 132:1-132:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{goy_et_al:LIPIcs.ICALP.2021.132,
  author =	{Goy, Alexandre and Petri\c{s}an, Daniela and Aiguier, Marc},
  title =	{{Powerset-Like Monads Weakly Distribute over Themselves in Toposes and Compact Hausdorff Spaces}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{132:1--132:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.132},
  URN =		{urn:nbn:de:0030-drops-142016},
  doi =		{10.4230/LIPIcs.ICALP.2021.132},
  annote =	{Keywords: Egli-Milner relation, weak extension, weak distributive law, weak lifting, powerset monad, Vietoris monad, topos, alternating automaton, generalized determinization}
}
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