Search Results

Documents authored by Jacobs, Jules

Document
DOI: 10.4230/LIPIcs.ECOOP.2026.17
NEST: Network Enforced Session Types

Authors: Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This paper introduces NEST (Network Enforced Session Types), a runtime verification framework that moves application-level protocol monitoring into the network fabric. Unlike prior work that instruments or wraps application code, we synthesise packet-level monitors that enforce protocols directly in the data plane. We develop algorithms to generate network-level monitors from session types and extend them to handle packet loss and reordering. We implement NEST in P4 and evaluate it on applications including microservice and network-function models, showing that network-level monitors can enforce realistic non-trivial protocols.
Cite as

Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 17:1-17:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.ECOOP.2026.17,
  author =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  title =	{{NEST: Network Enforced Session Types}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{17:1--17:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert 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.2026.17},
  URN =		{urn:nbn:de:0030-drops-261137},
  doi =		{10.4230/LIPIcs.ECOOP.2026.17},
  annote =	{Keywords: Session types, runtime verification, P4, programmable data planes}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.2
NEST: Network Enforced Session Types (Artifact)

Authors: Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
This artifact contains NEST: a tool for synthesizing network-level runtime monitors from application-level protocols specified as session types. More specifically, NEST takes as input one or more session types, and generates (1) a set of table entries to be uploaded on network switches that support the P4 standard, and (2) a Python API allowing applications to send/receive messages that carry the packet headers required for the network-level monitoring to work. This artifact also contains the code for reproducing the examples and measurements in the companion paper.
Cite as

Jens Kanstrup Larsen, Alceste Scalas, Guy Amir, Jules Jacobs, Jana Wagemaker, and Nate Foster. NEST: Network Enforced Session Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{larsen_et_al:DARTS.12.1.2,
  author =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  title =	{{NEST: Network Enforced Session Types (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Larsen, Jens Kanstrup and Scalas, Alceste and Amir, Guy and Jacobs, Jules and Wagemaker, Jana and Foster, Nate},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.2},
  URN =		{urn:nbn:de:0030-drops-261392},
  doi =		{10.4230/DARTS.12.1.2},
  annote =	{Keywords: Session types, runtime verification, P4, programmable data planes.}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.15
A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact)

Authors: Jules Jacobs

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
This is the artifact description for the paper "A Self-Dual Distillation of Session Types". The artifact consists of mechanized proofs of the theorems listed in the paper, in the Coq proof assistant.
Cite as

Jules Jacobs. A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{jacobs:DARTS.8.2.15,
  author =	{Jacobs, Jules},
  title =	{{A Self-Dual Distillation of Session Types: Mechanized Proofs (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Jacobs, Jules},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.15},
  URN =		{urn:nbn:de:0030-drops-162137},
  doi =		{10.4230/DARTS.8.2.15},
  annote =	{Keywords: Linear types, concurrency, lambda calculus, session types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.23
A Self-Dual Distillation of Session Types

Authors: Jules Jacobs

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We introduce ƛ ("lambda-barrier"), a minimal extension of linear λ-calculus with concurrent communication, which adds only a single new fork construct for spawning threads. It is inspired by GV, a session-typed functional language also based on linear λ-calculus. Unlike GV, ƛ strives to be as simple as possible, and adds no new operations other than fork, no new type formers, and no explicit definition of session type duality. Instead, we use linear function function type τ₁ -∘ τ₂ for communication between threads, which is dual to τ₂ -∘ τ₁, i.e., the function type constructor is dual to itself. Nevertheless, we can encode session types as ƛ types, GV’s channel operations as ƛ terms, and show that this encoding is type-preserving. The linear type system of ƛ ensures that all programs are deadlock-free and satisfy global progress, which we prove in Coq. Because of ƛ’s minimality, these proofs are simpler than mechanized proofs of deadlock freedom for GV.
Cite as

Jules Jacobs. A Self-Dual Distillation of Session Types. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jacobs:LIPIcs.ECOOP.2022.23,
  author =	{Jacobs, Jules},
  title =	{{A Self-Dual Distillation of Session Types}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{23:1--23:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.23},
  URN =		{urn:nbn:de:0030-drops-162518},
  doi =		{10.4230/LIPIcs.ECOOP.2022.23},
  annote =	{Keywords: Linear types, concurrency, lambda calculus, session types}
}
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