21 Search Results for "Mislove, Michael"

Document
DOI: 10.4230/LIPIcs.LICS.2026.59
Generalized Decidability via Brouwer Trees

Authors: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer tree ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for an ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀ i ∈ ℕ. P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.
Cite as

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg. Generalized Decidability via Brouwer Trees. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 59:1-59:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dejong_et_al:LIPIcs.LICS.2026.59,
  author =	{de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik},
  title =	{{Generalized Decidability via Brouwer Trees}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{59:1--59:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia 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.LICS.2026.59},
  URN =		{urn:nbn:de:0030-drops-268466},
  doi =		{10.4230/LIPIcs.LICS.2026.59},
  annote =	{Keywords: Decidability in constructive mathematics, homotopy type theory, ordinals, Brouwer trees, countable choice}
}
Document
DOI: 10.4230/OASIcs.NINeS.2026.3
Limix: Limiting Lamport Exposure to Distant Failures in Globally-Managed Distributed Systems

Authors: Cristina Băsescu, Georgia Fragkouli, Enis Ceyhun Alp, Michael F. Nowlan, Jose M. Faleiro, Gaylor Bosson, Kelong Cong, Pierluca Borsò-Tan, Vero Estrada-Galiñanes, and Bryan Ford

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

Abstract
Globalized computing infrastructures offer the convenience and elasticity of globally managed objects and services, but lack the resilience to distant failures that localized infrastructures such as private clouds provide. Providing both global management and resilience to distant failures, however, poses a fundamental problem for configuration services: How to discover a possibly migratory, strongly-consistent service/object in a globalized infrastructure without dependencies on globalized state? Limix is the first metadata configuration service that addresses this problem. With Limix, global strongly-consistent data-plane services and objects are insulated from remote gray failures by ensuring that the definitive, strongly-consistent metadata for any object is always confined to the same region as the object itself. Limix guarantees availability bounds: any user can continue accessing any strongly consistent object that matters to the user located at distance Δ away, insulated from failures outside a small multiple of Δ. We built a Limix metadata service based on the key-value interface of CockroachDB. Our experiments on Internet-like networks and on AWS, using realistic trace-driven workloads, show that Limix enables global management and significantly improves availability over the state-of-the-art.
Cite as

Cristina Băsescu, Georgia Fragkouli, Enis Ceyhun Alp, Michael F. Nowlan, Jose M. Faleiro, Gaylor Bosson, Kelong Cong, Pierluca Borsò-Tan, Vero Estrada-Galiñanes, and Bryan Ford. Limix: Limiting Lamport Exposure to Distant Failures in Globally-Managed Distributed Systems. In 1st New Ideas in Networked Systems (NINeS 2026). Open Access Series in Informatics (OASIcs), Volume 139, pp. 3:1-3:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{basescu_et_al:OASIcs.NINeS.2026.3,
  author =	{B\u{a}sescu, Cristina and Fragkouli, Georgia and Alp, Enis Ceyhun and Nowlan, Michael F. and Faleiro, Jose M. and Bosson, Gaylor and Cong, Kelong and Bors\`{o}-Tan, Pierluca and Estrada-Gali\~{n}anes, Vero and Ford, Bryan},
  title =	{{Limix: Limiting Lamport Exposure to Distant Failures in Globally-Managed Distributed Systems}},
  booktitle =	{1st New Ideas in Networked Systems (NINeS 2026)},
  pages =	{3:1--3:29},
  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.3},
  URN =		{urn:nbn:de:0030-drops-255880},
  doi =		{10.4230/OASIcs.NINeS.2026.3},
  annote =	{Keywords: Distributed systems, Availability, Fault tolerance, Strong-consistency, Coordination systems, Lamport exposure}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.47
Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors: Pablo Barenbaum, Delia Kesner, and Mariana Milicich

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

Abstract
Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.
Cite as

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
  author =	{Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
  title =	{{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{47:1--47:24},
  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.47},
  URN =		{urn:nbn:de:0030-drops-254721},
  doi =		{10.4230/LIPIcs.CSL.2026.47},
  annote =	{Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.48
Interpreting Lambda Calculus in Domain-Valued Random Variables

Authors: Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott

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

Abstract
We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.
Cite as

Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{furber_et_al:LIPIcs.CSL.2026.48,
  author =	{Furber, Robert and Mardare, Radu and Panangaden, Prakash and Scott, Dana},
  title =	{{Interpreting Lambda Calculus in Domain-Valued Random Variables}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{48:1--48:20},
  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.48},
  URN =		{urn:nbn:de:0030-drops-254734},
  doi =		{10.4230/LIPIcs.CSL.2026.48},
  annote =	{Keywords: lambda calculus, domain theory, random variables}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2026.4
Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk)

Authors: Pierre Clairambault

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

Abstract
Quantitative semantics are those denotational semantics that inherit from linear logic [Jean-Yves Girard, 1987] a sensitivity to the multiplicity of resources involved in computation. Those include the relational model [Jean-Yves Girard, 1987] and its numerous variations (such as finiteness spaces [Thomas Ehrhard, 2005], weighted relational models [Jim Laird et al., 2013] and their extensions [Thomas Ehrhard et al., 2011; Thomas Ehrhard, 2002], generalized species of structure [Fiore et al., 2008], span models [Paul-André Melliès, 2019; Pierre Clairambault and Simon Forest, 2023], etc), as well as related syntactic methods such as non-idempotent intersection types [Daniel de Carvalho, 2018] and Taylor expansion of lambda-terms [Thomas Ehrhard and Laurent Regnier, 2003]. Interactive semantics are usually also quantitative, but in addition they present the interactive behaviour of proofs and programs, generally organized chronologically - those include the many variants of game semantics (starting with [J. M. E. Hyland and C.-H. Luke Ong, 2000; Samson Abramsky et al., 2000]), and other frameworks such as Geometry of Interaction [Girard, 1989] or ludics [Jean-Yves Girard, 2001]. Both families are cornerstones of modern denotational semantics, and both have associated Alonzo Church awards: game semantics in 2017, and quantitative semantics (in particular, differential linear logic and the differential λ-calculus) in 2024. It has more or less always been clear to the experts that the two, sharing an origin in linear logic, are conceptually related. Yet there are differences, which seem fundamental: in particular, while quantitative models compose relationally, the composition of strategies follows an intricate "parallel interaction plus hiding" process inspired from concurrency theory [Abramsky, 1997]. The two families of models have also historically targeted different kinds of languages: whereas quantitative semantics focused on theoretical calculi (and the λ-calculus in particular), game semantics is known for fully abstract models for languages with elaborate combinations of effects including local state [Samson Abramsky and Guy McCusker, 1996], control operators [James Laird, 1997], and concurrent primitives [Dan R. Ghica and Andrzej S. Murawski, 2008]. Early on, researchers have explored the relationship between the two [Thomas Ehrhard, 1996; Patrick Baillot et al., 1997], and investigations on this question have spanned decades [Pierre Boudes, 2009; Ana C. Calderon and Guy McCusker, 2010; Takeshi Tsukada and C.-H. Luke Ong, 2016; C.-H. Luke Ong, 2017]. In particular, Melliès' work on asynchronous games [Paul-André Melliès, 2006; Paul-André Melliès, 2005] made significant conceptual contributions, showing that the issue was enlightened by adopting a positional formulation of game semantics, where points in the relational model simply arise as certain positions. This talk surveys recent developments in this line of work, shedding light on the connection between those two families. Our work is set in so-called "thin concurrent games" [Simon Castellan et al., 2019; Pierre Clairambault, 2024], an extension with symmetry of Rideau and Winskel’s concurrent games on event structures [Silvain Rideau and Glynn Winskel, 2011]. Event structures being one of the main "truly concurrent" models of concurrency [Glynn Winskel, 1986], it is perhaps expected that thin concurrent games can model concurrent languages: they provide a truly concurrent refinement of Ghica and Murawski’s fully abstract model of Idealized Concurrent Algol [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024]. But beyond the semantics of concurrency, thin concurrent games are also a deep reworking on game semantics built from causal principles, inheriting from asynchronous games a positional flavour. In thin concurrent games, strategies have a dual nature: an event-based nature where they appear as certain event structures composed via parallel interaction plus hiding; or a positional nature where they appear as certain spans of groupoids, composed by pullback (modulo a technical condition on strategies called visibility) - they can be regarded both as a games and a relational model! Leveraging this dual nature, in a sequence of papers with Castellan, de Visme, Olimpieri and Paquet, we have been able to link the single framework of thin concurrent games with numerous other models. This includes various traditional alternating or non-alternating games models [Simon Castellan and Pierre Clairambault, 2024; Pierre Clairambault, 2024], the weighted relational model [Pierre Clairambault and Hugo Paquet, 2021], the quantum relational model [Pierre Clairambault and Marc de Visme, 2020], generalized species of structure [Pierre Clairambault et al., 2023], and - going beyond quantitative semantics - the linear Scott model [Clairambault, 2025], a linear decomposition of standard Scott domain semantics [Thomas Ehrhard, 2012]. All these distinct models are obtained by projecting away certain aspects of thin concurrent games, giving some support to the claim that thin concurrent games are a Rosetta stone for interactive and quantitative semantics.
Cite as

Pierre Clairambault. Towards A Rosetta Stone of Interactive and Quantitative Semantics (Invited Talk). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{clairambault:LIPIcs.CSL.2026.4,
  author =	{Clairambault, Pierre},
  title =	{{Towards A Rosetta Stone of Interactive and Quantitative Semantics}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{4:1--4:4},
  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.4},
  URN =		{urn:nbn:de:0030-drops-254286},
  doi =		{10.4230/LIPIcs.CSL.2026.4},
  annote =	{Keywords: Denotational semantics, Game semantics}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2025.6
Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies

Authors: Pavel Hubáček, Jan Václavek, and Michelle Yeo

Published in: LIPIcs, Volume 361, 29th International Conference on Principles of Distributed Systems (OPODIS 2025)

Abstract
The rising importance of cryptocurrencies as financial assets pushed their applicability from an object of speculation closer to standard financial instruments such as loans. In this work, we initiate the study of secure protocols that enable fiat-denominated loans collateralized by cryptocurrencies such as Bitcoin. We provide limited-custodial protocols for such loans relying only on trusted arbitration and provide their game-theoretical analysis. We also highlight various interesting directions for future research.
Cite as

Pavel Hubáček, Jan Václavek, and Michelle Yeo. Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies. In 29th International Conference on Principles of Distributed Systems (OPODIS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 361, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hubacek_et_al:LIPIcs.OPODIS.2025.6,
  author =	{Hub\'{a}\v{c}ek, Pavel and V\'{a}clavek, Jan and Yeo, Michelle},
  title =	{{Foundations of Fiat-Denominated Loans Collateralized by Cryptocurrencies}},
  booktitle =	{29th International Conference on Principles of Distributed Systems (OPODIS 2025)},
  pages =	{6:1--6:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-409-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{361},
  editor =	{Arusoaie, Andrei and Onica, Emanuel and Spear, Michael and Tucci-Piergiovanni, Sara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2025.6},
  URN =		{urn:nbn:de:0030-drops-251796},
  doi =		{10.4230/LIPIcs.OPODIS.2025.6},
  annote =	{Keywords: Blockchains, Cryptocurrencies, DeFi, Loans, Mechanism design, Subgame Perfect Equilibrium, Rational analysis}
}
Document
DOI: 10.4230/LIPIcs.AFT.2025.28
Optimistic MEV in Ethereum Layer 2s: Why Blockspace Is Always in Demand

Authors: Ozan Solmaz, Lioba Heimbach, Yann Vonlanthen, and Roger Wattenhofer

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)

Abstract
Layer 2 rollups are rapidly absorbing DeFi activity, securing over $40 billion and accounting for nearly half of Ethereum’s DEX volume by Q1 2025, yet their MEV dynamics remain understudied. We address this gap by defining and quantifying optimistic MEV, a form of speculative, on-chain MEV whose detection and execution logic reside largely on-chain in smart contracts. As a result of their speculative nature and lack of off-chain opportunity verification, optimistic MEV transactions frequently decide not to execute any trades. In this work, we focus on cyclic arbitrage, which we find is predominantly executed as optimistic MEV on Layer 2s. Using our multi-stage identification pipeline on Arbitrum, Base, and Optimism, we show that in Q1 2025, transactions from cyclic arbitrage contracts account for over 50% of on-chain gas on Base and Optimism and 7% on Arbitrum, driven mainly by "interaction" probes (on-chain computations searching for arbitrage). This speculative probing indicates that cyclic arbitrage on Layer 2s is predominantly executed as optimistic MEV and contributes to generally keeping blocks on Base and Optimism persistently full. Despite consuming over half of on-chain gas, these optimistic MEV transactions pay less than one quarter of total gas fees. Cross-network comparison reveals divergent success rates, differing patterns of code reuse, and sensitivity to varying sequencer ordering and block production times. Finally, OLS regressions link optimistic MEV trade count to ETH volatility, retail trading activity, and DEX aggregator usage. Together, these findings show that optimistic MEV has become a major source of persistent spam-like transaction activity on Layer 2s, dominating blockspace with low-value probes and reshaping the composition of on-chain activity.
Cite as

Ozan Solmaz, Lioba Heimbach, Yann Vonlanthen, and Roger Wattenhofer. Optimistic MEV in Ethereum Layer 2s: Why Blockspace Is Always in Demand. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 28:1-28:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{solmaz_et_al:LIPIcs.AFT.2025.28,
  author =	{Solmaz, Ozan and Heimbach, Lioba and Vonlanthen, Yann and Wattenhofer, Roger},
  title =	{{Optimistic MEV in Ethereum Layer 2s: Why Blockspace Is Always in Demand}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{28:1--28:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.28},
  URN =		{urn:nbn:de:0030-drops-247479},
  doi =		{10.4230/LIPIcs.AFT.2025.28},
  annote =	{Keywords: blockchain, MEV, Layer 2, Ethereum}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.23
First-Order Store and Visibility in Name-Passing Calculi

Authors: Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.
Cite as

Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-Order Store and Visibility in Name-Passing Calculi. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2025.23,
  author =	{Hirschkoff, Daniel and Qu\'{e}merais, Iwan and Sangiorgi, Davide},
  title =	{{First-Order Store and Visibility in Name-Passing Calculi}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.23},
  URN =		{urn:nbn:de:0030-drops-239737},
  doi =		{10.4230/LIPIcs.CONCUR.2025.23},
  annote =	{Keywords: process calculi, behavioural equivalence, type system}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.12
Cancellative Convex Semilattices

Authors: Ana Sokolova and Harald Woracek

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad. A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations). We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).
Cite as

Ana Sokolova and Harald Woracek. Cancellative Convex Semilattices. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sokolova_et_al:LIPIcs.CALCO.2025.12,
  author =	{Sokolova, Ana and Woracek, Harald},
  title =	{{Cancellative Convex Semilattices}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.12},
  URN =		{urn:nbn:de:0030-drops-235714},
  doi =		{10.4230/LIPIcs.CALCO.2025.12},
  annote =	{Keywords: convex semilattice, cancellativity, Riesz space}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.3
Unsolvable Terms in Filter Models (Invited Talk)

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell

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

Abstract
Intersection type theories (itt’s) and filter models, i.e. λ-calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most λ-calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables.
Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable Terms in Filter Models (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:LIPIcs.FSCD.2025.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Honsell, Furio},
  title =	{{Unsolvable Terms in Filter Models}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{3:1--3:24},
  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.3},
  URN =		{urn:nbn:de:0030-drops-236181},
  doi =		{10.4230/LIPIcs.FSCD.2025.3},
  annote =	{Keywords: \lambda-calculus, Intersection Types, Unsolvable Terms, Filter Models}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.4
Separating Terms by Means of Multi Types, Coinductively

Authors: Adrienne Lancelot

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system. We prove a folklore result: weak head type equivalence coincides with Sangiorgi’s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence. The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.
Cite as

Adrienne Lancelot. Separating Terms by Means of Multi Types, Coinductively. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot:LIPIcs.TYPES.2024.4,
  author =	{Lancelot, Adrienne},
  title =	{{Separating Terms by Means of Multi Types, Coinductively}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.4},
  URN =		{urn:nbn:de:0030-drops-233660},
  doi =		{10.4230/LIPIcs.TYPES.2024.4},
  annote =	{Keywords: lambda calculus, intersection types, program equivalence}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.146
Saturation Problems for Families of Automata

Authors: León Bohn, Yong Li, Christof Löding, and Sven Schewe

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Families of deterministic finite automata (FDFA) represent regular ω-languages through their ultimately periodic words (UP-words). An FDFA accepts pairs of words, where the first component corresponds to a prefix of the UP-word, and the second component represents a period of that UP-word. An FDFA is termed saturated if, for each UP-word, either all or none of the pairs representing that UP-word are accepted. We demonstrate that determining whether a given FDFA is saturated can be accomplished in polynomial time, thus improving the known PSPACE upper bound by an exponential. We illustrate the application of this result by presenting the first polynomial learning algorithms for representations of the class of all regular ω-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular ω-languages when they are not saturated, we also address the regularity problem and show that it is PSPACE-complete. Finally, we explore a variant of FDFAs called families of deterministic weak automata (FDWA), where the semantics for the periodic part of the UP-word considers ω-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular ω-languages, and we compare the succinctness of these different models.
Cite as

León Bohn, Yong Li, Christof Löding, and Sven Schewe. Saturation Problems for Families of Automata. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 146:1-146:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.ICALP.2025.146,
  author =	{Bohn, Le\'{o}n and Li, Yong and L\"{o}ding, Christof and Schewe, Sven},
  title =	{{Saturation Problems for Families of Automata}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{146:1--146:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.146},
  URN =		{urn:nbn:de:0030-drops-235239},
  doi =		{10.4230/LIPIcs.ICALP.2025.146},
  annote =	{Keywords: Families of Automata, automata learning, FDFAs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.30
A Complete Inference System for Probabilistic Infinite Trace Equivalence

Authors: Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova

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

Abstract
We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.
Cite as

Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CSL.2025.30,
  author =	{C\^{i}rstea, Corina and Moss, Lawrence S. and Noquez, Victoria and Schmid, Todd and Silva, Alexandra and Sokolova, Ana},
  title =	{{A Complete Inference System for Probabilistic Infinite Trace Equivalence}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{30:1--30: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.30},
  URN =		{urn:nbn:de:0030-drops-227870},
  doi =		{10.4230/LIPIcs.CSL.2025.30},
  annote =	{Keywords: Coalgebra, infinite trace, semantics, logic, convex sets}
}
Document
Early Ideas
DOI: 10.4230/LIPIcs.CALCO.2021.18
The Central Valuations Monad (Early Ideas)

Authors: Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract
We give a commutative valuations monad Z on the category DCPO of dcpo’s and Scott-continuous functions. Compared to the commutative valuations monads given in [Xiaodong Jia et al., 2021], our new monad Z is larger and it contains all push-forward images of valuations on the unit interval [0, 1] along lower semi-continuous maps. We believe that this new monad will be useful in giving domain-theoretic denotational semantics for statistical programming languages with continuous probabilistic choice.
Cite as

Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev. The Central Valuations Monad (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 18:1-18:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{jia_et_al:LIPIcs.CALCO.2021.18,
  author =	{Jia, Xiaodong and Mislove, Michael and Zamdzhiev, Vladimir},
  title =	{{The Central Valuations Monad}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{18:1--18:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio 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.CALCO.2021.18},
  URN =		{urn:nbn:de:0030-drops-153733},
  doi =		{10.4230/LIPIcs.CALCO.2021.18},
  annote =	{Keywords: Valuations, Commutative Monad, DCPO, Probabilistic Choice, Recursion}
}
Document
DOI: 10.4230/DagRep.2.8.99
Information Flow and Its Applications (Dagstuhl Seminar 12352)

Authors: Samson Abramsky, Jean Krivine, and Michael W. Mislove

Published in: Dagstuhl Reports, Volume 2, Issue 8 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12352 "Information Flow and Its Applications". This seminar brought together mathematicians, computer scientists, physicists and researchers from related disciplines such as computational biology who are working on problems concerning information and information flow.
Cite as

Samson Abramsky, Jean Krivine, and Michael W. Mislove. Information Flow and Its Applications (Dagstuhl Seminar 12352). In Dagstuhl Reports, Volume 2, Issue 8, pp. 99-112, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{abramsky_et_al:DagRep.2.8.99,
  author =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  title =	{{Information Flow and Its Applications (Dagstuhl Seminar 12352)}},
  pages =	{99--112},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{8},
  editor =	{Abramsky, Samson and Krivine, Jean and Mislove, Michael W.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.8.99},
  URN =		{urn:nbn:de:0030-drops-37866},
  doi =		{10.4230/DagRep.2.8.99},
  annote =	{Keywords: Information flow; semantics of computation; quantum computing; systems biology; information theory; informatics}
}
  • Refine by Type
  • 21 Document/PDF
  • 12 Document/HTML

  • Refine by Publication Year
  • 6 2026
  • 7 2025
  • 1 2021
  • 1 2013
  • 1 2010
  • Show More...

  • Refine by Author
  • 4 Kovar, Martin
  • 2 Mislove, Michael
  • 2 Mislove, Michael W.
  • 2 Sokolova, Ana
  • 1 Abramsky, Samson
  • Show More...

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

  • Refine by Classification
  • 3 Theory of computation → Denotational semantics
  • 3 Theory of computation → Lambda calculus
  • 3 Theory of computation → Type theory
  • 2 Applied computing → Electronic commerce
  • 2 Computer systems organization → Distributed architectures
  • Show More...

  • Refine by Keyword
  • 2 domain theory
  • 2 lambda calculus
  • 1 (filtered) compactness
  • 1 (quasi-) sober space
  • 1 Availability
  • 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