
The SICSA Theme Event: "Practical Types" will be on 46 June 2014, hosted at The Burn near Brechin.
Foreword
The Practical Types Brainstorming Event is a joint event organised by the universities of Dundee, St Andrews and Strathclyde to discuss future collaborations on the topic "Types in functional programming languages".
Types have gone beyond merely labelling values, and are now seen as intrinsically defining properties of code,
both functional (what does a value represent) and extrafunctional (what program behaviour is implied
by a program term). Modern concepts of e.g. dependent types, session types, type classes, generic algebraic
data types (GADTs), gradual typing ... show great promise
in terms of describing and reasoning about program properties. However, there is still a significant gap between the
stateoftheart in type theory and the practical application of types in programming languages.
Scottish researchers have been at the forefront of advances in type theory and its application.
This 3day residential workshop aims to bring together researchers from across SICSA who are interested in issues of how to make
types practical. Topics of interest include, but are not limited to:
 use of types for describing and reasoning about functional/extrafunctional properties
 typebased static analyses, including amortised analysis
 types and concurrency, including session types
 types and safety/security
 proof carrying code
 application of categorical concepts in practical type settings
 types and generic programming
 type checking and type inference, including efficiency and other concerns
 static versus dynamic typing, including gradual typing
 design of typed languages
Organisers:
Neil Ghani,
Kevin Hammond, and
Katya Komendantskaya.
Programme
Participants and Contributed talks:

Stevan Andjelkovic (U.Strathclyde).

Guillaume Allais (U. Strathclyde).
 Alwin Blok (U.Strathclyde).

Roy Dyckhoff (U.St Andrews).

Fredrik Nordvall Forsberg
(U.Strathclyde)
Title: Inductiveinductive definitions in MartinLöf Type Theory. Abstract: MartinLöf's dependent type theory can be seen as a
functional programming language with a very rich type system. Of
course, we want this language to have a rich notion of data
structure as well. I will describe one class of such data types
which I studied during my PhD, where a type A is formed inductively,
simultaneously with a second type B : A > Type which depend on it.
Both types are formed inductively, hence we call such definitions
inductiveinductive definitions. I will give several examples of
inductiveinductive definitions, and discuss their metatheory.
 Marco Gaboardi (U.Dundee)
Title: Type checking linear dependent types for sensitivity.
Abstract: Recent works have shown the power of linear indexed type systems for capturing complex safety properties. These systems combine linear type systems with a language of indices that appear in the types, allowing more finegrained analysis. For example, linear indexed types have been fruitfully applied to verify differential privacy in the Fuzz type system.
A natural way to enhance the expressiveness of this approach is by allowing the indices to depend on runtime information, in the spirit of dependent types. This approach is used in DFuzz, an extension of Fuzz. The DFuzz type system relies on an indexlevel language supporting real and natural number arithmetic over con stants and dependent variables. Moreover, DFuzz uses a subtyping mechanism to semantically manipulate indices. By themselves, lin earity, dependency, and subtyping each require delicate handling when performing type checking or type inference; their combination increases this challenge substantially, as the features can interact in nontrivial ways.
In this talk, I will present the typechecking problem for DFuzz. I will show how one can reduce type checking for (a simple extension of) DFuzz to constraint solving over a firstorder theory of naturals and real numbers which, although undecidable, can often be handled in practice by standard numeric solvers.

Neil Ghani (U.Strathclyde).
Title: Logical Relations  Fibrationally.

Adam Gundry (WellTyped LLP).

Kevin Hammond (U.St Andrews).
Title: Dependent Types for Parallelism.
 Muhannad Hijaze (Herriot Watt).
 Katya Komendantskaya (U.Dundee).
Title: Coalgebraic Logic Programming for Type Inference.

Clemens Kupke (U.Strathclyde).
 Sam Lindley (U.Edinburgh).
Title: Effect Handlers for Idioms and Arrows.

Conor McBride (U.Strathclyde)
Title: "Functions as Handlers in Frank".
Abstract:
I can (if it seems appropriate and time permits) report on recent developments in the design of Frank, an effectsandhandlers programming language I've been working on with Sam Lindley. We've done away with a separate ""handler"" construct for effects by extending the ordinary language of function definition to cover a more interesting range of interactions with the process that computes the arguments. Accepting values from the arguments becomes a common special case. It's fun to build coroutines this way.
 Federico Orsanigo (U.Strathclyde).
Bifibrational Parametricity (with Neil Ghani, Patricia Johann, Fredrik
Nordvall Forsberg and Tim Revell).
Reynolds' theory of parametric polymorphism captures the invariance
of polymorphically typed programs under change of data
representation. Reflexive graph categories and fibrations give a
categorical understanding of parametric polymorphism.
In our work we contibute further to this categorical perspective on
parametricity
by showing the relevance of bifibrations.
In this talk I will illustrate, with the help of a concrete example,
our framework for parametric models of System F
and show how it allows conceptually simple statements of key lemmas
such as the Identity
Extension Lemma and Reynold's Abstraction Theorem.

Timothy Revell (U.Strathclyde)
Title: Fibrational Units of Measure. Abstract: In this talk I will give categorical semantics for
Andrew Kennedy’s Units of Measure (1998). I'll start by following the
standard approach in categorical logical and
type theory by using a fibrational structure to separate
indexinformation (the units) from indexedinformation (the types which
may contain units). This will lead us to the notion of a UoMfibration.
I'll give examples of UoM fibrations, including a model based upon
Gsets, and theorems allowing the construction of further
UoMfibrations. Finally, I'll touch on parametricity in this setting.
 Christopher Schwaab (U.St Andrews).
 Jerry Swan (U.Stirling)
 Matus Tejiscak (U.St Andrews).
Schedule
Wednesday 4th June
13:00  14:00  LUNCH  
14:00  15:30  Session 1.  
 
Welcome and Introduction. 
  Kevin Hammond. Dependent types for parallelism. 
  Discussion 
15:30  16:00  COFFEE  
16:00  17:30  Session 2.  
  Neil Ghani. Logical Relations  Fibrationally. 
  Marco Gaboardi. Type checking linear dependent types for sensitivity. 
  Discussion 
18:30   DINNER  
Thursday 5th June
8:00  9:30  BREAKFAST  . 
9:30  11:00  Contributed talks and discussion  . 
11:00  11:30  COFFEE  . 
11:30  13:00  Contributed talks and discussion  . 
13:00  14:00  LUNCH  . 
14:00  15:30  Contributed talks and discussion  . 
15:30  16:00  COFFEE  . 
16:00  17:30  Contributed talks and discussion  . 
18:30   DINNER  . 
Friday 6th June
8:00  9:30  BREAKFAST  . 
9:30  11:00  Contributed talks and discussion  . 
11:00  11:30  COFFEE  . 
11:30  13:00  Contributed talks and discussion  . 
13:00  14:00  LUNCH  . 
Important Dates
Event Dates: 4th6th June 2014
Deadline for Registration: 16 May 2014
Registration
If you plan to attend the event, please register here.
We do not charge a registration fee.
The Burn offers rates £60 for shared rooms and £75 for rooms with single occupancy, all meals included. Payments can be made at the Burn.
There will be a limited amount of funds available to cover the above costs; they will be allocated on the firstcomefirstserved basis.
Location
The Burn
Glenesk
Brechin
Angus DD9 7YP
Google Map
Travel Information
You can get to the Burn by taking a train to Montrose and then a bus to
Edzell (in Angus) and finally walking, cycling, or taking a taxi for the
last 1 and a half miles.
Equipment and Computing Facilities
The Seminar Room contains a whiteboard, OHP and Data Projector.
