Department of Computing Science, University of Glasgow
Room F121, Sir Alwyn Williams Building, Lilybank Gardens, Glasgow G12 8RZ.
Information on travelling to the university can be found here. Campus maps can be found here.
12.30 Lunch
14.00 Totality versus Turing Completeness
Conor McBride, University of Strathclyde
It's a well known fact that a total programming language can't encode its own interpreter. Some advocates and most detractors of total programming note that it comes at the cost of Turing Completeness, another well known fact. These well known facts are about as true as the fact that "Haskell can't handle I/O." I shall talk about ways in which total languages can model the risk of nontermination, and show you a method I have found useful, inspired by notions of algebraic effect.
14.45 Experiments in standard library design with Plaid
Iain McGinniss, University of Glasgow
Plaid is an object-functional, optionally typed dynamic language with deeply integrated typestate features, developed by Jonathan Aldrich et. al at Carnegie Mellon University. This novel combination of language features offers an interesting research opportunity to explore the design space of a standard library. Standard libraries in modern languages are expected to include robust and efficient data structures and IO abstractions (amongst many other things), provided in an idiomatic manner, exploiting the full set of features of the language. This talk will give a brief introduction to Plaid, and outline the design considerations made in the implementation of Plaid's current standard library.
15.30 Tea/coffee break
16.00 Handlers in Action
Ohad Kammar, University of Edinburgh
We present a small-step operational semantics for a simplified Call-by-Push-Value variant of Bauer and Pretnar's Eff programming language. Eff incorporates functional and imperative features by adapting Plotkin and Pretnar's effect handlers as a programming paradigm.
This is preliminary work with Sam Lindley and Nicolas Oury.
16.45 Linear Types in Programming Languages: Progress and Prospects
Simon Gay, University of Glasgow
The publication of Girard's original paper on linear logic, in 1987, provoked immediate interest in developing linear type systems by applying the Curry-Howard isomorphism. So why has linear typing not appeared as a standard feature of mainstream programming languages, in the way that parametric polymorphism has?
In this talk I will explore this theme, commenting on past, present and future uses of linear types in programming languages.17.30 End