SICSA Theme Event: "Practical Types"



The SICSA Theme Event: "Practical Types" will be on 4-6 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 extra-functional (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 state-of-the-art 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 3-day 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/extra-functional properties
  • type-based 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: Inductive-inductive definitions in Martin-Löf Type Theory. Abstract: Martin-Lö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 inductive-inductive definitions. I will give several examples of inductive-inductive definitions, and discuss their meta-theory.

  • 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 fine-grained 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 index-level 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 non-trivial ways. In this talk, I will present the type-checking problem for DFuzz. I will show how one can reduce type checking for (a simple extension of) DFuzz to constraint solving over a first-order 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 (Well-Typed 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 effects-and-handlers 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 index-information (the units) from indexed-information (the types which may contain units). This will lead us to the notion of a UoM-fibration. I'll give examples of UoM fibrations, including a model based upon G-sets, and theorems allowing the construction of further UoM-fibrations. 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:00LUNCH
    14:00 - 15:30Session 1.
    Welcome and Introduction.
    Kevin Hammond. Dependent types for parallelism.
    Discussion
    15:30 - 16:00COFFEE
    16:00 - 17:30Session 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:30BREAKFAST .
    9:30 - 11:00Contributed talks and discussion.
    11:00 - 11:30COFFEE .
    11:30 - 13:00Contributed talks and discussion.
    13:00 - 14:00LUNCH.
    14:00 - 15:30Contributed talks and discussion.
    15:30 - 16:00COFFEE .
    16:00 - 17:30Contributed talks and discussion.
    18:30 -- DINNER .

    Friday 6th June

    8:00 - 9:30BREAKFAST .
    9:30 - 11:00Contributed talks and discussion.
    11:00 - 11:30COFFEE .
    11:30 - 13:00Contributed talks and discussion.
    13:00 - 14:00LUNCH.

    Important Dates

    Event Dates: 4th-6th 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 first-come-first-served 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.