Mathematically Structured Programming Group

Computer and Information Sciences

University of Strathclyde

Parametricity Workshop

22nd May 2013.
Department of Computer and Information Sciences.

The idea of the workshop is to get people actively working on parametricity or logical relations together to discuss the latest research, and new research directions, in this area.

The workshop is organised by Patricia Johann.
Email: patricia.johann *at* strath.ac.uk.

[SICSA logo]

This workshop is supported by the Scottish Informatics and Computer Science Alliance.

Schedule

Time Talk
9:30 - 10:00 Coffee
10:00 - 10:15 Welcome remarks & information about the day
Patricia Johann
10:15 - 11:15 Fibrational Parametricity
Neil Ghani

Parametricity is a fundamental concept within programming languages designed to capture the idea that programs map related inputs to related outputs. Originally formulated by John Reynolds in the 1970s, parametrictiy has been a key tool in reasoning about programming languages ever since. However, as programming languages have advanced, parametricity has struggled to keep up. I think that part of the reason for this is that its not really clear what parametricity really is. We have lots of specific constructions of what a parametric model is but no satisfying overarching theory which can then be instantiated to a variety of different settings (operations, game-theoretic, constructive, domain theoretic etc)

In this talk I'll explain some work we have been doing in Strathclyde recently whose goal is to suggest that while the usual semantics of programming languages can be given abstractly in terms of a categorical universe using concepts such as categories, functors and natural transformations, parametricity amounts to working in a fibrational universe consisting of fibred categories, fibred functors and fibred natural transformations.

11:15 - 12:15 Type Theory in Color
Guilhem Moulin
Dependent type-theory is on the verge of becoming the standard way to formalize mathematics at the same time as displacing traditional platforms for high-insurance programming. However, current implementations of type theory are still lacking, in the sense that some obvious truths require explicit proofs, making type-theory awkward to use for many applications, both in formalization and programming. In particular, notions of erasure are poorly supported. We will present an extension of type-theory with colored terms, color erasure and interpretation of colored types as predicates. The result is a more powerful type-theory: some definitions and proofs may be omitted as they become trivial, it becomes easier to program with precise types, and some parametricity results can be internalized.
12:15 - 2:30 Lunch & informal discussion
2:30 - 3:30 Combining parametricity and effects
Alex Simpson
3:30 - 5:30 Coffee & informal discussion
5:30 Drinks (venue(s) TBA)
7:00 Dinner (venue(s) TBA)

Workshop Dinner

TBA

Venue, Travel and Accommodation

The workshop will take place in Livingstone Tower, which is part of the University of Strathclyde. Livingstone Tower is in central Glasgow, near to Glasgow Queen Street station. Below are travel instructions from Queen Street station, and from Glasgow and Edinburgh airports. Edinburgh and Glasgow airports are both served by several international airlines, and flights are available to and from major international hubs.

Map

The following map shows several key locations (click on the link below the map for a larger picture):


View Parametricity Workshop in a larger map

Accomodation

A convenient place to stay was the Glasgow City Centre Premier Inn, just across the road from Strathclyde University.

From Glasgow Queen Street Station

Livingstone Tower is a few minutes walk from Queen Street Station in the centre of Glasgow. The map above shows the general area.

There is also an official university map.

From Glasgow Airport

For people arriving at Glasgow Airport, here are instructions on how to get into the city centre. Probably the easiest route is to take the airport bus (Service 500) to Buchanan Street Bus station, which is close to Queen Street Station, and then to walk or take a taxi from there. The airport bus costs £7.50 for an open return.

From Edinburgh Airport

For people arriving via Edinburgh Airport, the best route is to take the airport bus to Waverley Station in central Edinburgh and then take the train to Glasgow Queen Street. There are trains every 15 minutes during the day, and every half an hour after 18.30. Note that train travel before 9.30 and between 16.30 and 18.30 is peak time, and is more expensive.