20 Search Results for "Berger, Ulrich"

Document
DOI: 10.4230/LIPIcs.SEA.2026.2
Different Scales of Randomness: Empirical Mixing Times of the Edge Switching and Curveball MCMC

Authors: Deepak Ajwani, Melvin Kallmayer, Alexander Leonhardt, Ulrich Meyer, Ryan O'Connor, and Manuel Penschuck

Published in: LIPIcs, Volume 371, 24th International Symposium on Experimental Algorithms (SEA 2026)

Abstract
The Fixed Degree Sequence Model (FDSM) asks for a uniform sample from the set of all simple graphs that match a prescribed degree sequence. It is typically implemented using Markov-Chain Monte-Carlo (MCMC) processes, such as Edge Switching or Curveball (and their variants). Yet despite decades of research, rigorous bounds on the mixing times of such processes remain impractical. Consequently, several experimental techniques have been used to derive "empirical lower bounds" on the mixing time. We address the following research questions: (1) Which commonly studied graph-theoretic properties serve as reliable empirical predictors for mixing of FDSM MCMC processes? (2) At what structural scales do these properties operate primarily (i. e., are they predominantly local or global in nature)? (3) How can these properties be characterised and quantified most effectively? To this end, we propose Claim, a novel systematic method to establish empirical lower bounds using learnt classifiers, and compare it to existing methods. Apart from interesting insights into the usage of machine learning for this problem, we also derive robust graph properties with respect to different randomisation algorithms. Although experimental in nature, these results may influence both theorist’s and algorithm engineer’s work on improved bounds and better algorithm respectively.
Cite as

Deepak Ajwani, Melvin Kallmayer, Alexander Leonhardt, Ulrich Meyer, Ryan O'Connor, and Manuel Penschuck. Different Scales of Randomness: Empirical Mixing Times of the Edge Switching and Curveball MCMC. In 24th International Symposium on Experimental Algorithms (SEA 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 371, pp. 2:1-2:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ajwani_et_al:LIPIcs.SEA.2026.2,
  author =	{Ajwani, Deepak and Kallmayer, Melvin and Leonhardt, Alexander and Meyer, Ulrich and O'Connor, Ryan and Penschuck, Manuel},
  title =	{{Different Scales of Randomness: Empirical Mixing Times of the Edge Switching and Curveball MCMC}},
  booktitle =	{24th International Symposium on Experimental Algorithms (SEA 2026)},
  pages =	{2:1--2:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-422-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{371},
  editor =	{Aum\"{u}ller, Martin and Finocchi, Irene},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2026.2},
  URN =		{urn:nbn:de:0030-drops-260062},
  doi =		{10.4230/LIPIcs.SEA.2026.2},
  annote =	{Keywords: Mixing Time, Graph Randomization, Machine Learning, Edge Switching}
}
Document
DOI: 10.4230/OASIcs.AEiC.2026.4
HASCO: A Hybrid AI Simulation Compiler for Semantic Accident Reconstruction

Authors: Edin Jelačić, Rong Gu, Cristina Seceleanu, Ning Xiong, Peter Backeman, Tiberiu Seceleanu, Zhennan Fei, and Ali Nouri

Published in: OASIcs, Volume 143, 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026)

Abstract
The validation of Automated Driving Systems (ADSs) has shifted from distance-based metrics to Scenario-Based Testing (SBT). Large Language Models (LLMs) have emerged as powerful tools with potential for generating vehicular scenarios at scale. However, generative models, used for direct simulation synthesis, produce inadequate output, therefore necessitating a more structured compilation approach. In this regard, we present HASCO (Hybrid AI Simulation COmpiler), a system that translates natural-language driving scene specifications into executable simulation artifacts (XOSC/XODR files) for the esmini/OpenSCENARIO ecosystem. While LLMs excel at narrative parsing, we demonstrate that direct synthesis of simulation artifacts fails in the vast majority of cases due to hallucinated physics or schema violations. To resolve this, HASCO treats scenario creation as a compilation task rather than a generative one. The pipeline supports three compilation paths: direct synthesis, a Python intermediate (via scenariogeneration), and an ontology-guided path that grounds intent into an intermediate representation (IR) before compilation. We further evaluate a self-judging mechanism for automated repair. Across six operating modes evaluated on 40 real-world accident reports, the ontology-guided compiler and Python-based compiler achieve 95% and 90% executability rates, respectively (compared to 5% for direct synthesis). Additionally, we evaluate outputs on semantic fidelity, positioning HASCO as a robust tool for forensic scene reconstruction.
Cite as

Edin Jelačić, Rong Gu, Cristina Seceleanu, Ning Xiong, Peter Backeman, Tiberiu Seceleanu, Zhennan Fei, and Ali Nouri. HASCO: A Hybrid AI Simulation Compiler for Semantic Accident Reconstruction. In 30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026). Open Access Series in Informatics (OASIcs), Volume 143, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{jelacic_et_al:OASIcs.AEiC.2026.4,
  author =	{Jela\v{c}i\'{c}, Edin and Gu, Rong and Seceleanu, Cristina and Xiong, Ning and Backeman, Peter and Seceleanu, Tiberiu and Fei, Zhennan and Nouri, Ali},
  title =	{{HASCO: A Hybrid AI Simulation Compiler for Semantic Accident Reconstruction}},
  booktitle =	{30th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2026)},
  pages =	{4:1--4:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-425-3},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{143},
  editor =	{Filieri, Antonio and Backeman, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.AEiC.2026.4},
  URN =		{urn:nbn:de:0030-drops-259220},
  doi =		{10.4230/OASIcs.AEiC.2026.4},
  annote =	{Keywords: Autonomous Driving, OpenSCENARIO, Large Language Models, Scenario Generation, Semantic Reconstruction}
}
Document
DOI: 10.4230/OASIcs.NINeS.2026.21
Accio: Rethinking OS-Architecture Co-Design for Next-Gen I/O

Authors: Amirmohammad Nazari, Rajit Manohar, and Robert Soulé

Published in: OASIcs, Volume 139, 1st New Ideas in Networked Systems (NINeS 2026)

Abstract
In this paper, we propose a novel software/hardware design to improve I/O performance while maintaining existing POSIX-standard APIs. Our approach stands in contrast to existing kernel-bypass strategies that improve performance at the expense of abandoning familiar programming abstractions. Our key insight is that navigating the performance-functionality trade-off requires changes to the processor; it cannot be done without support of the CPU micro-architecture. Our design, called Accio, includes: dedicated hardware for interrupt management, a hardware assist for thread scheduling, tables in hardware that manage I/O state, and modifications to the operating system to support the new hardware. Our evaluation demonstrates that Accio saturates the bus bandwidth, reduces CPU usage by up to 66% compared to state-of-the-art kernel-bypass systems, and reduces latency to 1/12th of that of the Linux kernel, matching that of kernel-bypass systems.
Cite as

Amirmohammad Nazari, Rajit Manohar, and Robert Soulé. Accio: Rethinking OS-Architecture Co-Design for Next-Gen I/O. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{nazari_et_al:OASIcs.NINeS.2026.21,
  author =	{Nazari, Amirmohammad and Manohar, Rajit and Soul\'{e}, Robert},
  title =	{{Accio: Rethinking OS-Architecture Co-Design for Next-Gen I/O}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{21:1--21:24},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-414-7},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{139},
  editor =	{Argyraki, Katerina and Panda, Aurojit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.NINeS.2026.21},
  URN =		{urn:nbn:de:0030-drops-256063},
  doi =		{10.4230/OASIcs.NINeS.2026.21},
  annote =	{Keywords: Networks, Operating Systems, I/O Optimization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.19
A Unifying Conservation Theorem

Authors: Giulio Fellin

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

Abstract
The relationship between classical and constructive logics has long been illuminated by a series of conservation results, beginning with Kolmogorov’s negative translation and Glivenko’s double negation theorem, and later extended by Kuroda and Segerberg to first-order and minimal logics respectively. These results reveal how certain classical principles can be interpreted or recovered within weaker constructive frameworks, either via translations or through minimal extensions that satisfy specific logical properties. In this paper, we propose a unifying generalisation of these conservation theorems, that consolidates and expands the abstract methods introduced in earlier studies, offering a unified perspective on the interplay between classical provability and constructive reasoning.
Cite as

Giulio Fellin. A Unifying Conservation Theorem. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fellin:LIPIcs.CSL.2026.19,
  author =	{Fellin, Giulio},
  title =	{{A Unifying Conservation Theorem}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{19:1--19: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.19},
  URN =		{urn:nbn:de:0030-drops-254431},
  doi =		{10.4230/LIPIcs.CSL.2026.19},
  annote =	{Keywords: double negation, negative translation, conservation, minimal logic, Glivenko’s theorem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.22
On the Algorithmic Structure of Dialectica Realisers

Authors: Davide Barbarossa and Thomas Powell

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

Abstract
Gödel’s Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today’s proof mining program. In the past decades, it has also been studied from the perspective of programming languages, and our contribution is in that direction. Specifically, we present Dialectica as a collection of rules in the style of Hoare logic, where Dialectica is now viewed as a language for specifying procedural programs that come with a forward and backward direction. This viewpoint captures the interesting dynamics of realisers extracted by the Dialectica interpretation, and we illustrate this by defining a generalised backpropagation semantics for a fragment of this language. We envisage this work as providing a base for several future developments, both theoretical and practical, which we outline at the end.
Cite as

Davide Barbarossa and Thomas Powell. On the Algorithmic Structure of Dialectica Realisers. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barbarossa_et_al:LIPIcs.CSL.2026.22,
  author =	{Barbarossa, Davide and Powell, Thomas},
  title =	{{On the Algorithmic Structure of Dialectica Realisers}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{22:1--22:22},
  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.22},
  URN =		{urn:nbn:de:0030-drops-254466},
  doi =		{10.4230/LIPIcs.CSL.2026.22},
  annote =	{Keywords: Dialectica interpretation, Hoare logic, Programs from proofs}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.33
Digital Health for Space: Towards Prevention, Training, Empowerment, and Autonomy

Authors: Mario A. Cypko, Ulrich Straube, Russell J. Andrews, and Oliver Amft

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
Future long-duration and deep-space missions will rely on digital health technologies to ensure the health and safety of the crew, as well as to enable the required mission autonomy. This position paper redefines the current paradigms of digital health by emphasizing prevention, self-management, and individual empowerment for health as central challenges for both space and terrestrial medicine. We focus on future mission scenarios and highlight the potential of co-evolving digital health and related technologies, particularly sensing, artificial intelligence (AI), and human-computer interaction (HCI), across the continuum of space medicine: from astronaut selection and training to prevention, diagnostics, therapy, rehabilitation, and long-term care. Future digital health technologies can respond to pressing needs arising from limited medical infrastructure, rising care costs, and increasing demands on healthcare systems in space and on Earth. To structure research and development needs, we introduce a framework with four autonomy levels based on mission distance and communication latency (Earth orbit, Lunar Gateway and Moon vicinity, Mars, and deep space) that illustrate how mission context constrains medical support and dictates system requirements. Using the Lunar Orbital Platform-Gateway as a near-future reference, we discuss how growing communication delays demand greater onboard autonomy and new telemedical strategies. Within the proposed framework, we integrate solutions built around AI-supported decision making, multimodal monitoring, and adaptive HCI, which should be co-designed through human-centered methods to form a cohesive health management ecosystem. The framework opens up synergies for proactive and trustworthy health support under isolation and limited ground contact. The paper consolidates current technological readiness and strategic challenges, offering guidance for space health research and policy, with clear translational benefits for terrestrial care delivery.
Cite as

Mario A. Cypko, Ulrich Straube, Russell J. Andrews, and Oliver Amft. Digital Health for Space: Towards Prevention, Training, Empowerment, and Autonomy. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cypko_et_al:OASIcs.SpaceCHI.2025.33,
  author =	{Cypko, Mario A. and Straube, Ulrich and Andrews, Russell J. and Amft, Oliver},
  title =	{{Digital Health for Space: Towards Prevention, Training, Empowerment, and Autonomy}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{33:1--33:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.33},
  URN =		{urn:nbn:de:0030-drops-240236},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.33},
  annote =	{Keywords: Digital Health in Space, AI-based Decision Support, Wearable Health Monitoring, Human-Computer Interaction (HCI), Autonomous Medical Systems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.2
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk)

Authors: Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the "neural" and "symbolic" program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle - standing as an abbreviation for a "verification condition language" - an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle’s overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.
Cite as

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Ekaterina Komendantskaya, Natalia Slusarz, and Luca Arnaboldi. Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{daggitt_et_al:LIPIcs.FSCD.2025.2,
  author =	{Daggitt, Matthew L. and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca},
  title =	{{Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.2},
  URN =		{urn:nbn:de:0030-drops-236172},
  doi =		{10.4230/LIPIcs.FSCD.2025.2},
  annote =	{Keywords: Neural Network Verification, Types, Interactive Theorem Provers}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.34
Monad Translations for Higher-Order Logic

Authors: Thomas Traversié

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Classical logic can be embedded into intuitionistic logic by inserting double negations in formulas. Several translations generalize this idea by using monad operators instead of double negations. They eliminate particular axioms, for instance the principle of excluded middle or the principle of explosion, and therefore can be used to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic. Such translations have been defined for first-order logic. In this paper, we define a translation, parameterized by monad operators, for higher-order logic. In particular, the property that any formula and its translation are equivalent in the presence of the eliminated axiom holds under functional extensionality and propositional extensionality. We apply this translation to embed higher-order classical (respectively intuitionistic) logic into higher-order intuitionistic (respectively minimal) logic. By adapting Friedman’s trick, we show that coherent formulas correspond to a constructive fragment of higher-order classical logic, meaning that we can transform classical proofs into intuitionistic proofs without modifying the proven statements.
Cite as

Thomas Traversié. Monad Translations for Higher-Order Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{traversie:LIPIcs.FSCD.2025.34,
  author =	{Traversi\'{e}, Thomas},
  title =	{{Monad Translations for Higher-Order Logic}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{34:1--34:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.34},
  URN =		{urn:nbn:de:0030-drops-236495},
  doi =		{10.4230/LIPIcs.FSCD.2025.34},
  annote =	{Keywords: Higher-order logic, Intuitionistic logic, Kuroda’s translation, Monad}
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.10
Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.
Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.23
How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus

Authors: Rémy Cerda and Lionel Vaux Auclair

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Twenty years after its introduction by Ehrhard and Regnier, differentiation in λ-calculus and in linear logic is now a celebrated tool. In particular, it allows to write the Taylor formula in various λ-calculi, hence providing a theory of linear approximations for these calculi. In the standard λ-calculus, this linear approximation is expressed by results stating that the (possibly) infinitary β-reduction of λ-terms is simulated by the reduction of their Taylor expansion: in terms of rewriting systems, the resource reduction (operating on Taylor approximants) is an extension of the β-reduction. In this paper, we address the converse property, conservativity: are there reductions of the Taylor approximants that do not arise from an actual β-reduction of the approximated term? We show that if we restrict the setting to finite terms and β-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the β-reduction preserving good simulation properties. This restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier’s pioneering work.
Cite as

Rémy Cerda and Lionel Vaux Auclair. How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the λ-Calculus. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.STACS.2025.23,
  author =	{Cerda, R\'{e}my and Vaux Auclair, Lionel},
  title =	{{How to Play the Accordion: Uniformity and the (Non-)Conservativity of the Linear Approximation of the \lambda-Calculus}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.23},
  URN =		{urn:nbn:de:0030-drops-228480},
  doi =		{10.4230/LIPIcs.STACS.2025.23},
  annote =	{Keywords: program approximation, quantitative semantics, lambda-calculus, linear approximation, Taylor expansion, conservativity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.34
The Lambda Calculus Is Quantifiable

Authors: Valentin Maestracci and Paolo Pistone

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

Abstract
In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the λ-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the D_∞ model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a λ-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.
Cite as

Valentin Maestracci and Paolo Pistone. The Lambda Calculus Is Quantifiable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{maestracci_et_al:LIPIcs.CSL.2025.34,
  author =	{Maestracci, Valentin and Pistone, Paolo},
  title =	{{The Lambda Calculus Is Quantifiable}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{34:1--34: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.34},
  URN =		{urn:nbn:de:0030-drops-227911},
  doi =		{10.4230/LIPIcs.CSL.2025.34},
  annote =	{Keywords: Lambda-calculus, Scott semantics, Partial metric spaces, B\"{o}hm trees, Taylor expansion}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.41
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Authors: Tim S. Lyon, Ian Shillito, and Alwen Tiu

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

Abstract
It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.
Cite as

Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lyon_et_al:LIPIcs.CSL.2025.41,
  author =	{Lyon, Tim S. and Shillito, Ian and Tiu, Alwen},
  title =	{{Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{41:1--41: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.41},
  URN =		{urn:nbn:de:0030-drops-227987},
  doi =		{10.4230/LIPIcs.CSL.2025.41},
  annote =	{Keywords: Bi-intuitionistic, Cut-elimination, Conservativity, Domain, First-order, Polytree, Proof theory, Reachability, Sequent}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.1
Martin Hofmann’s Case for Non-Strictly Positive Data Types

Authors: Ulrich Berger, Ralph Matthes, and Anton Setzer

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.
Cite as

Ulrich Berger, Ralph Matthes, and Anton Setzer. Martin Hofmann’s Case for Non-Strictly Positive Data Types. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.TYPES.2018.1,
  author =	{Berger, Ulrich and Matthes, Ralph and Setzer, Anton},
  title =	{{Martin Hofmann’s Case for Non-Strictly Positive Data Types}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{1:1--1:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.1},
  URN =		{urn:nbn:de:0030-drops-114052},
  doi =		{10.4230/LIPIcs.TYPES.2018.1},
  annote =	{Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell}
}
Document
DOI: 10.4230/LIPIcs.DISC.2018.11
Integrated Bounds for Disintegrated Storage

Authors: Alon Berger, Idit Keidar, and Alexander Spiegelman

Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)

Abstract
We point out a somewhat surprising similarity between non-authenticated Byzantine storage, coded storage, and certain emulations of shared registers from smaller ones. A common characteristic in all of these is the inability of reads to safely return a value obtained in a single atomic access to shared storage. We collectively refer to such systems as disintegrated storage, and show integrated space lower bounds for asynchronous regular wait-free emulations in all of them. In a nutshell, if readers are invisible, then the storage cost of such systems is inherently exponential in the size of written values; otherwise, it is at least linear in the number of readers. Our bounds are asymptotically tight to known algorithms, and thus justify their high costs.
Cite as

Alon Berger, Idit Keidar, and Alexander Spiegelman. Integrated Bounds for Disintegrated Storage. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.DISC.2018.11,
  author =	{Berger, Alon and Keidar, Idit and Spiegelman, Alexander},
  title =	{{Integrated Bounds for Disintegrated Storage}},
  booktitle =	{32nd International Symposium on Distributed Computing (DISC 2018)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-092-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{121},
  editor =	{Schmid, Ulrich and Widder, Josef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.11},
  URN =		{urn:nbn:de:0030-drops-98009},
  doi =		{10.4230/LIPIcs.DISC.2018.11},
  annote =	{Keywords: storage, coding, lower bounds, space complexity, register emulations}
}
  • Refine by Type
  • 20 Document/PDF
  • 12 Document/HTML

  • Refine by Publication Year
  • 5 2026
  • 8 2025
  • 1 2019
  • 1 2018
  • 1 2016
  • Show More...

  • Refine by Author
  • 6 Berger, Ulrich
  • 2 Cerda, Rémy
  • 1 Ajwani, Deepak
  • 1 Amft, Oliver
  • 1 Andrews, Russell J.
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs
  • 5 OASIcs
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 5 Theory of computation → Proof theory
  • 3 Theory of computation → Constructive mathematics
  • 3 Theory of computation → Lambda calculus
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Program semantics
  • Show More...

  • Refine by Keyword
  • 3 Taylor expansion
  • 2 Agda
  • 2 Böhm trees
  • 2 Proof theory
  • 2 program approximation
  • 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