Building opening hours
The main entrance to the School of Computer Science is open 8:00–20:00 on weekdays.
Lunches take place in Café Aspire in the Amenities Building.
- Tue Aug 31
20:00- Some of us will be in the Three Wheatsheaves (a pub). You can have dinner there if you like.
- Wed Sep 1
9:00–10:00 Martin Churchill: Game Semantics and Agda 10:30–11:30 Makoto Takeyama: D-Case graphical editor to Agda connection 11:40–12:40 Computational Irrelevance, Program Extraction and Universe Polymorphism; discussion leader: Jean-Philippe Bernardy 12:40–13:40 Lunch 13:40–18:30 Code sprints, including coordination 19:00- Dinner at Mr Man’s Restaurant, we meet at 18:30 in the Hub.
- Thu Sep 2
9:00–10:00 Andreas Abel: Positivity checking with polarized types 10:00–12:20 Code sprints 12:20–13:20 Lunch 13:20–18:30 Code sprints 19:30- Dinner at Kayal, we meet at 18:45 in the Hub.
- Fri Sep 3
9:00–10:00 Edwin Brady: Optimising dependent types 10:00–12:20 Code sprints 12:20–13:20 Lunch 13:20–18:00 Code sprints 18:30- Dinner at The Wollaton, we meet at 18:00 in the Hub.
- Sat Sep 4
Excursion (estimated times).
(If people want to spend more time in Castleton we can also return later.)
9:00–9:30 Bus from P&J, Bus from Jubilee campus 9:45–11:47 Train, Nottingham-Sheffield-Edale (£11.40 return); note that you have to pay a penalty if you board without a ticket 11:47–13:00 Lunch, Edale 13:00–16:00 Walk: Edale-Hollins Cross-Great Ridge-Lose Hill-Castleton (weather forecast) 16:00–18:00 Dinner, Castleton 18:00–18:56 Bus, Castleton-Sheffield (return tickets for the train should be valid on the bus) 19:05–20:00 Train, Sheffield-Nottingham
- Sun Sep 5 No group activities planned (yet).
- Mon Sep 6
9:00–10:00 Discussion: Future development of Agda FutureOfAgda 10:00–11:20 Code sprints 11:20–12:20 Anton Setzer: Coalgebras in dependent type theory - the saga continues Slides 12:20–13:20 Lunch 13:20–18:30 Code sprints 19:00- Dinner in the Three Wheatsheaves, we meet in the Hub at 18:30
- Tue Sep 7
9:00–10:00 Progress report on Epigram 10:00–12:00 Code Sprints 12:00–12:20 Discussion about AIM XIII and AIM XIV 12:20–13:20 Lunch 13:20–14:00 Code sprints 14:00–17:00 Code sprint debriefing
- Jean-Philippe Bernardy Computational Irrelevance, as implemented in Coq, is a useful feature. Marking code as computationally irrelevant is useful as a design tool, and also gives additional benefits, like the possibility of extraction of programs from proofs. A downside of the Coq approach is that the code is potentially duplicated in both sides of the relevance barrier. An adaptation of the experimental universe-polymorphism feature of Agda can provide the benefits of computational irrelevance, without paying the cost of code duplication. I propose to present a case for that feature and discuss the feasibility with Agda implementers.
- Edwin Brady I’d like to give a short talk about the forcing, detagging and collapsing optimisations (as described in my thesis and implemented in Idris) and discuss how these may be implemented in Agda, with the goal of improving the efficiency of the type checker by reducing sharing. (And, hopefully, actually implement it!)
- Martin Churchill Game models provide denotational (compositional) semantics for a wide variety of languages, including those with computational effects including higher-order store. These models are usually fully abstract. We describe the foundations of a formulation of game semantics in Agda, based on a type-theoretic representation rather than the usual set of traces. We describe the category of games in Agda, and give the denotational semantics of a small imperative language. We can then use the computational content of the Agda formulation to “run” the denotational semantics, giving a way of exploring interactions between these open terms and their environment. Joint work with Makoto Takeyama.
- Anton Setzer We look again at how to represent weakly final coalgebras in dependent type theory. We investigate how to interpret the nesting of coalgebras and algebras, and connections to object oriented (or better object based) programming. Finally we show how to give a semantics to weakly final coalgebras.