Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Thu 27 Sep 2018 15:30 - 15:50 at New York Central - Error Messages & Contexts Chair(s): David Darais

In normal typed λ-calculi, variables may be used multiple times, in multiple contexts, for multiple reasons, as long as the types agree. The disciplines of linear types and coeffects refine this by tracking how variables are used. For instance, we might track how many times a variable is used, or whether it is used covariantly, contravariantly, or invariantly. Such a discipline yields a general framework of “context constrained computing”, where constraints on variables in the context tell us something interesting about the computation being performed.

We will present work in progress on capturing the “intensional” properties of programs via a family of Kripke indexed relational semantics that refines a simple set-theoretic semantics of programs. The value of our approach lies in its generality and the range of examples covered.

Context Constrained Computing (tyde18-paper15.pdf)559KiB

Thu 27 Sep

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 16:10
Error Messages & ContextsTyDe at New York Central
Chair(s): David Darais University of Vermont
15:30
20m
Talk
Extended Abstract: Context Constrained Computing
TyDe
Robert Atkey University of Strathclyde, James Wood University of Strathclyde
File Attached
15:50
20m
Talk
Extended Abstract: Improving Error Messages for Dependent Types
TyDe
Joseph Eremondi University of British Columbia, Wouter Swierstra Utrecht University, Netherlands, Jurriaan Hage Utrecht University
File Attached