Program etc.

Wireless access

Use either UoN-guest or eduroam.

Building opening hours

The main entrance to the School of Computer Science is open 8:00–20:00 on weekdays.

Notes

Notes from the meeting.

Program

Talks, discussions and code sprints take place in room C1 in the Computer Science building.

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:00Martin Churchill: Game Semantics and Agda
    10:30–11:30Makoto Takeyama: D-Case graphical editor to Agda connection
    11:40–12:40Computational Irrelevance, Program Extraction and Universe Polymorphism; discussion leader: Jean-Philippe Bernardy
    12:40–13:40Lunch
    13:40–18:30Code 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:00Andreas Abel: Positivity checking with polarized types
    10:00–12:20Code sprints
    12:20–13:20Lunch
    13:20–18:30Code sprints
    19:30-Dinner at Kayal, we meet at 18:45 in the Hub.
  • Fri Sep 3
    9:00–10:00Edwin Brady: Optimising dependent types
    10:00–12:20Code sprints
    12:20–13:20Lunch
    13:20–18:00Code sprints
    18:30-Dinner at The Wollaton, we meet at 18:00 in the Hub.
  • Sat Sep 4
    Excursion (estimated times).
    9:00–9:30Bus from P&J, Bus from Jubilee campus
    9:45–11:47Train, Nottingham-Sheffield-Edale (£11.40 return); note that you have to pay a penalty if you board without a ticket
    11:47–13:00Lunch, Edale
    13:00–16:00Walk: Edale-Hollins Cross-Great Ridge-Lose Hill-Castleton (weather forecast)
    16:00–18:00Dinner, Castleton
    18:00–18:56Bus, Castleton-Sheffield (return tickets for the train should be valid on the bus)
    19:05–20:00Train, Sheffield-Nottingham
    (If people want to spend more time in Castleton we can also return later.)
  • Sun Sep 5
    No group activities planned (yet).
  • Mon Sep 6
    9:00–10:00Discussion: Future development of Agda FutureOfAgda
    10:00–11:20Code sprints
    11:20–12:20Anton Setzer: Coalgebras in dependent type theory - the saga continues Slides
    12:20–13:20Lunch
    13:20–18:30Code sprints
    19:00-Dinner in the Three Wheatsheaves, we meet in the Hub at 18:30
  • Tue Sep 7
    9:00–10:00Progress report on Epigram
    10:00–12:00Code Sprints
    12:00–12:20Discussion about AIM XIII and AIM XIV
    12:20–13:20Lunch
    13:20–14:00Code sprints
    14:00–17:00Code sprint debriefing

Abstracts

  • 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.