Write a Blog >>
Sat 23 Jan 2016 14:00 - 14:45 at Room St Petersburg I - Session Three Chair(s): Limin Jia

A good abstraction or two can be invaluable for programming, enabling reasoning, performance, and maintainability. We build abstractions by erecting barriers to the flow of information between implementations and their clients.

John Reynolds’ theory of relational parametricity seeks to explain abstraction in terms of invariance under change. Reynolds’ original theory explains abstract types by modelling change of representation types by mathematical relations. In essence, we have successfully maintained a barrier to information flow if the program is invariant under all changes of representation that act identically given the information they are permitted to have.

In this talk, I’ll present some ways of generalising Reynolds’ theory to novel applications by considering alternative notions of change. Change in space and time yields applications to geometry and classical mechanics. Considering changes as distances affords quantitative accounting of information flow. Indexed and dependent types allow programmers more precision in describing changes and so more precision is defining abstractions.

Sat 23 Jan
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

14:00 - 15:35: Off the Beaten Track - Session Three at Room St Petersburg I
Chair(s): Limin JiaCarnegie Mellon University
OBT-2016-talks14:00 - 14:45
Robert AtkeyUniversity of Strathclyde
OBT-2016-talks14:45 - 15:10
OBT-2016-talks15:10 - 15:35