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: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).

  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

  (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: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

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.