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]](sicsalogo.jpg)
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):
- Livingstone Tower, where the workshop took place.
- Glasgow City Centre Premier Inn, the recommended accommodation.
- Glasgow Queen Street Station, for people arriving by train or from Edinburgh airport (see below).
- Buchanan Bus Station, for people arriving from Glasgow Airport (see below).
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.
- General instructions on how to get into city centre
- Instructions on the bus service from the airport
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.
- General instructions on travel to and from Edinburgh airport
- Edinburgh airport bus for getting from Edinburgh Airport to Waverley Station.
- Edinburgh Waverley Station for general information.
- National Rail Website for train times.