xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Tue 24 Aug 2021 19:45 - 20:00 at ICFP Talks - Session 4
Wed 25 Aug 2021 07:45 - 08:00 at ICFP Talks - Session 4

Despite the great success of inferring and programming with
universal types, their dual—existential types—are much harder
to work with. Existential types are useful in building abstract types,
working with indexed types, and providing first-class
support for refinement types. This paper, set in the context of Haskell,
presents a bidirectional type-inference algorithm that infers where to introduce
and eliminate existentials without any annotations in terms, along with
an explicitly typed, type-safe core language usable as a compilation target.
This approach is backward compatible. The key ingredient is to use \emph{strong}
existentials, which support (lazily) projecting out the encapsulated data,
not weak existentials accessible only by pattern-matching.

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