Date/Time
Date(s) - 21/10/2015
11:00 am - 5:30 pm
Location
University of Edinburgh, Informatics Forum
The Scottish Programming Languages Seminar is an informal meeting for the discussion of any aspect of programming languages. The next SPLS will take place on Wednesday 21 October 2015 at the University of Edinburgh.
Information and updates about the October edition of SPLS will be sent via the SPLS Mailing List.
If you plan on attending, please register here.
We gratefully acknowledge financial support from the Complex Systems Engineering theme of SICSA.
Confirmed Speakers
Danel Ahman (University of Edinburgh) — Dependent Types and Fibred Computational Effects
Guillaume Allais (University of Strathclyde) — Type and Scope Preserving Semantics
James Chapman (University of Strathclyde) — Relative Monads
Aaron Crane (Cutbot) — Writing immutable software in a mutable language
Charles Grellois (University of Dundee) — Linear logic, duality, and higher-order model-checking
Shayan Najd (University of Edinburgh) — Quoted Domain-Specific Languages, an Interesting Spot in the Design Space
Roly Perera (University of Glasgow) — Behavioural Prototypes
Matúš Tejiščák (University of St Andrews) — Erasure in dependently typed functional languages
Programme
The meeting will begin at 11AM and last until 17:30. There will be lunch, talks, coffee breaks, and a visit to a nearby pub.
10:30 – 11:00: Early Arrivals Coffee
11:00 – 12:30: Session 1
11:00 – 11:45: James Chapman — Relative Monads
Relative Monads are a naturally arising relaxation of the monads where the underlying functor need not be an endofunctor. I will describe relative monads and their surrounding theory, and give examples of their use in Agda and Haskell.
11:45 – 12:30: Aaron Crane — Writing immutable software in a mutable language
Languages like Haskell and Idris view immutability of data as a property of the language. Proponents of this approach point out advantages like the ease of reasoning about program behaviour, especially for data that is used across concurrency boundaries.
This talk offers an alternative view of the world: that software designs can get huge benefit from relying on immutable data even when the implementation uses a language designed around mutable data. While this is not an entirely novel position, it is backed up here by a case study of a piece of real-world industrial software, written in Perl, that extracts rich information from web pages published by the Scottish and UK parliaments. Perl is a highly dynamic language; it strongly favours the flexibility and convenience offered by that approach over both theoretical purity and the ability to make static guarantees about program behaviour. This talk examines how the design of the Cutbot software makes the most of both mutable and immutable data — even in the absence of language support for guaranteeing immutability.
12:30 – 13:30: Lunch
13:30 – 14:30: Session 2
13:30 – 14:00: Shayan Najd — Quoted Domain-Specific Languages, an Interesting Spot in the Design Space
14:00 – 14:30: Guillaume Allais — Type and Scope Preserving Semantics
We introduce a notion of type and scope preserving semantics generalising Goguen and McKinna’s approach to defining one traversal generic enough to be instantiated to renaming first and then substitution. Its careful distinctionof environment and model values as well as its variation on a structure typical of a Kripke semantics make it capable of expressing renaming and substitution but also various forms of Normalisation by Evaluation as well as, perhaps more surprisingly, monadic computations such as a printing function.
We then demonstrate that expressing these algorithms in a common frameworkyields immediate benefits: we can deploy some logical relations generically overthese instances and obtain for instance the fusion lemmas for renaming, substitution and normalisation by evaluation as simple corollaries of the appropriatefundamental lemma.
14:30 – 15:00: Coffee
15:00 – 16:00: Session 3
15:00 – 15:30: Danel Ahman — Dependent Types and Fibred Computational Effects
In this talk I will discuss the interplay between two important topics in programming language research: dependent types and computational effects; by defining a small dependently-typed language, combining the features of Martin-Löf type theory and computational languages such as Call-By-Push-Value and the Enriched Effect Calculus. Our language has both value types and terms and computation types and terms, with the value and computation types only allowed to depend on values. A novel aspect of our language is the use of computational sigma-types to account for type-dependency in the sequential composition of computations.
The design of our language is inspired by a class of categorical models we call fibred adjunction models. These naturally combine i) comprehension categories arising from the semantics of dependent types; and ii) adjunctions arising from the semantics of computational effects. We also discuss a variety of examples, some arising from EM-algebras of monads, some from other decompositions of monads into adjunctions and some from considering general recursion as a computational effect.
Finally, we also comment on some ongoing work on understanding parametrized adjunctions and parametrized computational effects in this fibred setting. In particular, we show how the clear distinction between values and computations sheds new light on how to model parametrized computational effects where the result parameters need to depend on the values returned by the program, for example, to model the possible failure of opening a file.
(Joint work with Neil Ghani and Gordon Plotkin.)
15:30 – 16:00: Matúš Tejiščák — Erasure in dependently typed functional languages
16:00 – 16:30: Coffee
16:30 – 17:30: Session 4
16:30 – 17:00: Charles Grellois — Linear logic, duality, and higher-order model-checking
A common approach in verification, model-checking consists in computing whether a given formula holds on an abstract model of interest — typically, on a tree of actions representing the set of executions of a program. Over such a tree, a common procedure is to execute an automaton which checks whether an associated formula is satisfied.
The model-checking of functional programs requires a careful treatment of higher-order recursive computation, which is a major hurdle to the traditional abstraction of programs as finite graphs, and thus to a decidability result. This led to the use of semantic methods, notably in Ong’s decidability proof (2006).
In this talk, we explain how linear logic leads to a new insight into the higher-order model-checking problem, notably as it discloses very naturally the dual behavior of the program and of its automata-theoretic specification. From this observation, we extend models of linear logic to obtain a purely semantic account of Ong’s result: a given property over the set of executions of the program is satisfied if and only if the semantic interaction of the program with the automaton encoding the property of interest contains the initial state of the automaton.
This is joint work with my PhD advisor Paul-André Melliès.
17:00 – 17:30: Roly Perera — Behavioural Prototypes
Venue and Travel
SPLS will take place at the Informatics Forum, 10 Crichton Street, Edinburgh. The entrance is opposite that of Appleton Tower; the rooms used for the seminar and lunches will be signposted.
