License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2020.14
URN: urn:nbn:de:0030-drops-131717
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13171/
Go to the corresponding LIPIcs Volume Portal

Fowler, Simon

Model-View-Update-Communicate: Session Types Meet the Elm Architecture

pdf-format:
LIPIcs-ECOOP-2020-14.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{fowler:LIPIcs:2020:13171,
  author =	{Simon Fowler},
  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 =	{Robert Hirschfeld and Tobias Pape},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13171},
  URN =		{urn:nbn:de:0030-drops-131717},
  doi =		{10.4230/LIPIcs.ECOOP.2020.14},
  annote =	{Keywords: Session types, concurrent programming, Model-View-Update}
}

Keywords: Session types, concurrent programming, Model-View-Update
Collection: 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Issue Date: 2020
Date of publication: 06.11.2020
Supplementary Material: ECOOP 2020 Artifact Evaluation approved artifact available at https://doi.org/10.4230/DARTS.6.2.13.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI