7 Search Results for "Bengtson, Jesper"

Document
DOI: 10.4230/LIPIcs.ITP.2025.30
Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors: Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.
Cite as

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.ITP.2025.30,
  author =	{Silva, Rafael Castro Gon\c{c}alves and Fernet, Laouen and Traytel, Dmitriy},
  title =	{{Nondeterministic Asynchronous Dataflow in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.30},
  URN =		{urn:nbn:de:0030-drops-246280},
  doi =		{10.4230/LIPIcs.ITP.2025.30},
  annote =	{Keywords: dataflow, verification, coinduction, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.11
Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

Authors: Jan van Brügge, Andrei Popescu, and Dmitriy Traytel

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Nominal Isabelle provides powerful tools for meta-theoretic reasoning about syntax of logics or programming languages, in which variables are bound. It has been instrumental to major verification successes, such as Gödel’s incompleteness theorems. However, the existing tooling is not compositional. In particular, it does not support nested recursion, linear binding patterns, or infinitely branching syntax. These limitations are fundamental in the way nominal datatypes and functions on them are constructed within Nominal Isabelle. Taking advantage of recent theoretical advancements that overcome these limitations through a modular approach using the concept of map-restricted bounded natural functor (MRBNF), we develop and implement a new definitional package for binding-aware datatypes in Isabelle/HOL, called MrBNF. We describe the journey from the user specification to the end-product types, constants and theorems the tool generates. We validate MrBNF in two formalization case studies that so far were out of reach of nominal approaches: (1) Mazza’s isomorphism between the finitary and the infinitary affine λ-calculus, and (2) the POPLmark 2B challenge, which involves non-free binders for linear pattern matching.
Cite as

Jan van Brügge, Andrei Popescu, and Dmitriy Traytel. Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbrugge_et_al:LIPIcs.ITP.2025.11,
  author =	{van Br\"{u}gge, Jan and Popescu, Andrei and Traytel, Dmitriy},
  title =	{{Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.11},
  URN =		{urn:nbn:de:0030-drops-246091},
  doi =		{10.4230/LIPIcs.ITP.2025.11},
  annote =	{Keywords: syntax with bindings, datatypes, inductive predicates, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.30
Open Bisimilarity for the π-Calculus with Mismatch

Authors: Tiange Liu, Alwen Tiu, and Ross Horne

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

Abstract
Open bisimilarity is an equivalence relation for the π-calculus that is also congruence, making it suitable to use in compositional reasoning for mobile processes and communication protocols. The original definition of open bisimilarity, due to Sangiorgi, does not account for the mismatch operator, that is crucial in modelling real-world protocols. When mismatch is present, the congruence property no longer holds for open bisimilarity. In a LICS 2018 paper, Horne et al. proposed an extension of open bisimilarity, using a history-indexed class of relations, to address this problem. That definition, however, turns out to be non-compositional as we shall demonstrate in this paper. This paper presents a new definition of open bisimilarity in the π-calculus that incorporates mismatch. This is achieved by augmenting the transition semantics of the π-calculus with an explicit assumption about name distinctions, and by requiring that open bisimulation to be closed under an arbitary extension of the name distinctions assumption. We then prove that the resulting open bisimilarity is both an equivalence relation and a congruence.
Cite as

Tiange Liu, Alwen Tiu, and Ross Horne. Open Bisimilarity for the π-Calculus with Mismatch. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CONCUR.2025.30,
  author =	{Liu, Tiange and Tiu, Alwen and Horne, Ross},
  title =	{{Open Bisimilarity for the \pi-Calculus with Mismatch}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{30:1--30:20},
  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.30},
  URN =		{urn:nbn:de:0030-drops-239805},
  doi =		{10.4230/LIPIcs.CONCUR.2025.30},
  annote =	{Keywords: mismatch, open bisimilarity, pi calculus}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.31
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

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

Abstract
Session types offer a type-based approach to describing the message exchange protocols between participants in communication-based systems. Initially, they were introduced in a binary setting, specifying communication patterns between two components. With the advent of multiparty session types (MPST), the typing discipline was extended to arbitrarily many components. In MPST, communication patterns are given in terms of global types, an Alice-Bob notation that gives a global view of how components interact. A central theorem of MPST is subject reduction: a well-typed system remains well-typed after reduction. The literature contains some formulations of MPST with proofs of subject reduction that have later been shown to be incorrect. In this paper, we show that the subject reduction proof of the original formulation of MPST by Honda et al. contains some flaws. Additionally, we provide a restriction to the theory and show that, for this fragment, subject reduction does indeed hold. Finally, we use subject reduction to show that well-typed processes never go wrong. All of our proofs are mechanised using the Coq proof assistant.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 31:1-31:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tirore_et_al:LIPIcs.ECOOP.2025.31,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{31:1--31:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.31},
  URN =		{urn:nbn:de:0030-drops-233238},
  doi =		{10.4230/LIPIcs.ECOOP.2025.31},
  annote =	{Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.3
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Session types offer a type-based approach to describing the message exchange protocols between participants in communication-based systems. Initially, they were introduced in a binary setting, specifying communication patterns between two components. With the advent of multiparty session types (MPST), the typing discipline was extended to arbitrarily many components. In MPST, communication patterns are given in terms of global types, an Alice-Bob notation that gives a global view of how components interact. A central theorem of MPST is subject reduction: a well-typed system remains well-typed after reduction. The literature contains some formulations of MPST with proofs of subject reduction that have later been shown to be incorrect. In this paper, we show that the subject reduction proof of the original formulation of MPST by Honda et al. contains some flaws. Additionally, we provide a restriction to the theory and show that, for this fragment, subject reduction does indeed hold. Finally, we use subject reduction to show that well-typed processes never go wrong. All of our proofs are mechanised using the Coq proof assistant. This artifact accompanies our paper [Dawit Tirore et al., 2025]. It contains the Coq mechanisation of the theory described therein.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{tirore_et_al:DARTS.11.2.3,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact)}},
  pages =	{3:1--3:5},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.3},
  URN =		{urn:nbn:de:0030-drops-233467},
  doi =		{10.4230/DARTS.11.2.3},
  annote =	{Keywords: Session types, Multiparty, Mechanisation, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.28
A Sound and Complete Projection for Global Types

Authors: Dawit Tirore, Jesper Bengtson, and Marco Carbone

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role. Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.
Cite as

Dawit Tirore, Jesper Bengtson, and Marco Carbone. A Sound and Complete Projection for Global Types. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tirore_et_al:LIPIcs.ITP.2023.28,
  author =	{Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
  title =	{{A Sound and Complete Projection for Global Types}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.28},
  URN =		{urn:nbn:de:0030-drops-184039},
  doi =		{10.4230/LIPIcs.ITP.2023.28},
  annote =	{Keywords: Session types, Mechanisation, Projection, Coq}
}
  • Refine by Type
  • 7 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 6 2025
  • 1 2023

  • Refine by Author
  • 3 Bengtson, Jesper
  • 3 Carbone, Marco
  • 3 Tirore, Dawit
  • 2 Traytel, Dmitriy
  • 1 Fernet, Laouen
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 DARTS

  • Refine by Classification
  • 3 Theory of computation → Process calculi
  • 2 Security and privacy → Logic and verification
  • 2 Theory of computation → Program specifications
  • 2 Theory of computation → Type structures
  • 1 Computing methodologies → Distributed algorithms
  • Show More...

  • Refine by Keyword
  • 3 Coq
  • 3 Mechanisation
  • 3 Session types
  • 2 Isabelle/HOL
  • 2 Multiparty
  • 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact