ICFP 2021
Sun 22 - Sat 28 August 2021
Tue 24 Aug 2021 19:30 - 19:45 at ICFP Talks - Session 4
Wed 25 Aug 2021 07:30 - 07:45 at ICFP Talks - Session 4

Actors collaborate via message exchanges to reach a common goal. Experience has shown, however, that pure message-based communication is limiting and forces developers to use design patterns. The recently introduced dataspace actor model borrows ideas from the tuple space realm. It offers a tightly controlled, shared storage facility for groups of actors. In this model, actors assert facts that they wish to share and interests in such assertions. The dataspace notifies interested parties of changes to the set of assertions that they are interested in. Although it is straightforward to add the dataspace model to untyped languages, adding a typed interface is both necessary and challenging. Without restrictions on exchanged data, a faulty actor may propagate erroneous data through a malformed assertion, causing an otherwise well-behaved actor to crash—violating the key principle of failure isolation. A properly designed type system can prevent this scenario and rule out other kinds of uncooperative actors. This paper presents the first structural type system for the dataspace model of actors; it does not address the question of behavioral types for assertion-oriented protocols.

Tue 24 Aug

Displayed time zone: Seoul change

19:00 - 20:45
19:00
15m
Talk
How to design co-programs (JFP Presentation)
Research Papers
Jeremy Gibbons Department of Computer Science, University of Oxford
Link to publication DOI Media Attached
19:15
15m
Talk
A Theory of Higher-Order Subtyping with Type Intervals
Research Papers
Sandro Stucki Chalmers | University of Gothenburg, Paolo G. Giarrusso Delft University of Technology
DOI Pre-print Media Attached
19:30
15m
Talk
Typed dataspace actors (JFP Presentation)
Research Papers
Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
19:45
15m
Talk
An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper
Research Papers
Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee
DOI Media Attached
20:00
15m
Talk
Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)
Research Papers
Andrzej Filinski DIKU, University of Copenhagen
Link to publication DOI Media Attached
20:15
15m
Talk
Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI Pre-print Media Attached
20:30
15m
Talk
Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)
Research Papers
Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh
Link to publication DOI Media Attached

Wed 25 Aug

Displayed time zone: Seoul change

07:00 - 08:45
Session 4Research Papers at ICFP Talks
07:00
15m
Talk
How to design co-programs (JFP Presentation)
Research Papers
Jeremy Gibbons Department of Computer Science, University of Oxford
Link to publication DOI Media Attached
07:15
15m
Talk
A Theory of Higher-Order Subtyping with Type Intervals
Research Papers
Sandro Stucki Chalmers | University of Gothenburg, Paolo G. Giarrusso Delft University of Technology
DOI Pre-print Media Attached
07:30
15m
Talk
Typed dataspace actors (JFP Presentation)
Research Papers
Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University
Link to publication DOI Media Attached
07:45
15m
Talk
An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper
Research Papers
Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee
DOI Media Attached
08:00
15m
Talk
Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)
Research Papers
Andrzej Filinski DIKU, University of Copenhagen
Link to publication DOI Media Attached
08:15
15m
Talk
Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI Pre-print Media Attached
08:30
15m
Talk
Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)
Research Papers
Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh
Link to publication DOI Media Attached