Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Wed 21 Sep 2016 15:30 - 15:55 at Noh Theater - Session 11 Chair(s): Alejandro Russo

We present a linear functional calculus with both the safety guarantees expressible with linear types and the rich language of combinators and composition provided by functional programming. Unlike previous combinations of linear typing and functional programming, we compromise neither the linear side (for example, our linear values are first-class citizens of the language) nor the functional side (for example, we do not require duplicate definitions of compositions for linear and unrestricted functions). To do so, we must generalize abstraction and application to encompass both linear and unrestricted functions. We capture the typing of the generalized constructs with a novel use of qualified types. Our system maintains the metatheoretic properties of the theory of qualified types, including principal types and decidable type inference. Finally, we give a formal basis for our claims of expressiveness, by showing that evaluation respects linearity, and that our language is a conservative extension of existing functional calculi.

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

15:05 - 16:20
Session 11Research Papers at Noh Theater
Chair(s): Alejandro Russo Chalmers University of Technology
15:05
25m
Talk
Talking Bananas: Structural Recursion for Session Types
Research Papers
Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Edinburgh, UK
DOI
15:30
25m
Talk
The Best of Both Worlds: Linear Functional Programming without Compromise
Research Papers
J. Garrett Morris University of Edinburgh, UK
DOI
15:55
25m
Talk
Context-Free Session Types
Research Papers
Peter Thiemann University of Freiburg, Germany, Vasco Thudichum Vasconcelos
DOI