Search Results

Documents authored by Fowler, Simon

Document
DOI: 10.4230/LIPIcs.CONCUR.2021.36
Separating Sessions Smoothly

Authors: Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and strong normalisation. HGV exploits hyper-environments, which are collections of type environments, to ensure that structural congruence is type preserving. As a consequence we obtain a tight operational correspondence between HGV and HCP, a hypersequent-based process-calculus interpretation of classical linear logic. Our translations from HGV to HCP and vice-versa both preserve and reflect reduction. HGV scales smoothly to support Girard’s Mix rule, a crucial ingredient for channel forwarding and exceptions.
Cite as

Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating Sessions Smoothly. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fowler_et_al:LIPIcs.CONCUR.2021.36,
  author =	{Fowler, Simon and Kokke, Wen and Dardha, Ornela and Lindley, Sam and Morris, J. Garrett},
  title =	{{Separating Sessions Smoothly}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.36},
  URN =		{urn:nbn:de:0030-drops-144138},
  doi =		{10.4230/LIPIcs.CONCUR.2021.36},
  annote =	{Keywords: session types, hypersequents, linear lambda calculus}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.8
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Artifact)

Authors: Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
This is the companion artifact for the paper "Multiparty Session Types for Safe Runtime Adaptation in an Actor Language". EnsembleS is an actor-based programming language supporting dynamic self-adaptation, (discovery, replacement, and communication), which also guarantees communication safety. The artifact includes the EnsembleS compiler, the modified StMungo code, and all examples contained within the paper.
Cite as

Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{harvey_et_al:DARTS.7.2.8,
  author =	{Harvey, Paul and Fowler, Simon and Dardha, Ornela and Gay, Simon J.},
  title =	{{Multiparty Session Types for Safe Runtime Adaptation in an Actor Language (Artifact)}},
  pages =	{8:1--8:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Harvey, Paul and Fowler, Simon and Dardha, Ornela and Gay, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.2.8},
  URN =		{urn:nbn:de:0030-drops-140327},
  doi =		{10.4230/DARTS.7.2.8},
  annote =	{Keywords: Concurrency, session types, adaptation, actors, trust}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.10
Multiparty Session Types for Safe Runtime Adaptation in an Actor Language

Authors: Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Human fallibility, unpredictable operating environments, and the heterogeneity of hardware devices are driving the need for software to be able to adapt as seen in the Internet of Things or telecommunication networks. Unfortunately, mainstream programming languages do not readily allow a software component to sense and respond to its operating environment, by discovering, replacing, and communicating with components that are not part of the original system design, while maintaining static correctness guarantees. In particular, if a new component is discovered at runtime, there is no guarantee that its communication behaviour is compatible with existing components. We address this problem by using multiparty session types with explicit connection actions, a type formalism used to model distributed communication protocols. By associating session types with software components, the discovery process can check protocol compatibility and, when required, correctly replace components without jeopardising safety. We present the design and implementation of EnsembleS, the first actor-based language with adaptive features and a static session type system, and apply it to a case study based on an adaptive DNS server. We formalise the type system of EnsembleS and prove the safety of well-typed programs, making essential use of recent advances in non-classical multiparty session types.
Cite as

Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 10:1-10:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{harvey_et_al:LIPIcs.ECOOP.2021.10,
  author =	{Harvey, Paul and Fowler, Simon and Dardha, Ornela and Gay, Simon J.},
  title =	{{Multiparty Session Types for Safe Runtime Adaptation in an Actor Language}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{10:1--10:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.10},
  URN =		{urn:nbn:de:0030-drops-140539},
  doi =		{10.4230/LIPIcs.ECOOP.2021.10},
  annote =	{Keywords: Concurrency, session types, adaptation}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.13
Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact)

Authors: Simon Fowler

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Model-View-Update (MVU) is a development pattern for user interfaces pioneered by the Elm programming language. In the accompanying paper, we show a theoretical model of MVU, and detail how it can be extended to support session-typed communication. This artifact consists of a Docker image which contains a version of the Links programming language, equipped with an MVU library supporting session-typed communication. The implementation is showcased by all examples provided in the paper, alongside larger examples including a two-factor authentication workflow and multi-room chat server.
Cite as

Simon Fowler. Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{fowler:DARTS.6.2.13,
  author =	{Fowler, Simon},
  title =	{{Model-View-Update-Communicate: Session Types Meet the Elm Architecture (Artifact)}},
  pages =	{13:1--13:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Fowler, Simon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.13},
  URN =		{urn:nbn:de:0030-drops-132109},
  doi =		{10.4230/DARTS.6.2.13},
  annote =	{Keywords: Session types, concurrent programming, Model-View-Update}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.14
Model-View-Update-Communicate: Session Types Meet the Elm Architecture

Authors: Simon Fowler

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Session types are a type discipline for communication channel endpoints which allow conformance to protocols to be checked statically. Safely implementing session types requires linearity, usually in the form of a linear type system. Unfortunately, linear typing is difficult to integrate with graphical user interfaces (GUIs), and to date most programs using session types are command line applications. In this paper, we propose the first principled integration of session typing and GUI development by building upon the Model-View-Update (MVU) architecture, pioneered by the Elm programming language. We introduce λMVU, the first formal model of the MVU architecture, and prove it sound. By extending λMVU with commands as found in Elm, along with linearity and model transitions, we show the first formal integration of session typing and GUI programming. We implement our approach in the Links web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.
Cite as

Simon Fowler. Model-View-Update-Communicate: Session Types Meet the Elm Architecture. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 14:1-14:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fowler:LIPIcs.ECOOP.2020.14,
  author =	{Fowler, Simon},
  title =	{{Model-View-Update-Communicate: Session Types Meet the Elm Architecture}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{14:1--14:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.14},
  URN =		{urn:nbn:de:0030-drops-131717},
  doi =		{10.4230/LIPIcs.ECOOP.2020.14},
  annote =	{Keywords: Session types, concurrent programming, Model-View-Update}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.11
Mixing Metaphors: Actors as Channels and Channels as Actors

Authors: Simon Fowler, Sam Lindley, and Philip Wadler

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Channel- and actor-based programming languages are both used in practice, but the two are often confused. Languages such as Go provide anonymous processes which communicate using buffers or rendezvous points---known as channels---while languages such as Erlang provide addressable processes---known as actors---each with a single incoming message queue. The lack of a common representation makes it difficult to reason about translations that exist in the folklore. We define a calculus lambda-ch for typed asynchronous channels, and a calculus lambda-act for typed actors. We define translations from lambda-act into lambda-ch and lambda-ch into lambda-act and prove that both are type- and semantics-preserving. We show that our approach accounts for synchronisation and selective receive in actor systems and discuss future extensions to support guarded choice and behavioural types.
Cite as

Simon Fowler, Sam Lindley, and Philip Wadler. Mixing Metaphors: Actors as Channels and Channels as Actors. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fowler_et_al:LIPIcs.ECOOP.2017.11,
  author =	{Fowler, Simon and Lindley, Sam and Wadler, Philip},
  title =	{{Mixing Metaphors: Actors as Channels and Channels as Actors}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{11:1--11:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.11},
  URN =		{urn:nbn:de:0030-drops-72536},
  doi =		{10.4230/LIPIcs.ECOOP.2017.11},
  annote =	{Keywords: Actors, Channels, Communication centric Programming Languages}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact