Agda Implementors' Meeting XXVIII

The twenty-eighth Agda Implementors' Meeting will be held in Nottingham, United Kingdom at the university's school of computer science from 15 Oct 2018 to 20 Oct 2018 (Monday to Saturday). The plan is to have:

  • Talks and presentations about the theory, implementation, and use cases of Agda.
  • Many discussions about Agda, including potential new features, goals, milestones.
  • Plenty of time to work on or in Agda, in collaboration with the other participants.

Important dates

Registration deadline

The deadline is soft, and if you miss it, you will still be very welcome to come. However, it will be helpful for planning if you let Nicolai know that you intend to come. A short email is enough; of course, you can still make suggestions afterwards.

2018-10-15 (Mon) to 2018-10-20 (Sat)

Caveat: Visa

Britain is NOT in the Schengen area! If you have an EU passport/ID card, this is not a problem (at least until early next year and hopefully afterwards); otherwise, you might need an additional visa. Please contact Nicolai if you need help.


Please register for this meeting by filling out the form below and sending it to Nicolai.

There is no registration fee. Coffee breaks may be included (probably they are). Transportation, accommodation and meals are to be covered by the participant. There will (probably) be an excursion which may cause additional costs for the participants as well (details to be determined).

    Registration form
    Agda Implementors' Meeting XXVIII


    Title and optionally abstract (if you want to give a talk or lead a discussion; optional):

    Suggestions for code sprints (optional):

    Additional comments (optional):


  • Gun Pinyo
  • John Leo
  • Thorsten Altenkirch
  • Paolo Capriotti
  • Jakob von Raumer
  • Filippo Sestini
  • Nicolai Kraus
  • Jesper Cockx
  • Matthew Daggitt
  • Niels van der Weide
  • ...

Daily Schedule



Presentations on theory, implementation, and use cases of Agda and type theory are welcome. If you would like to give a presentation, please write to Nicolai.

  • Niels: Eliminating Traversals in Agda

Brief Abstract: We discuss a formalization of Bird's ‘replaceMin’ program (replaces all values in a tree by the minimum in one traversal) in Agda using Sized Types.

Detailed program


Code sprint suggestions

  • John: Edit-time tactics
  • Rethinking interleaving of functions and datatypes (Issue #2858).
  • Matthew: Making in-file pragmas consistent across files, e.g. --safe, --without-k (Issue #2487)
  • ...

Wrap up meetings

A short summary of the daily progress will be added.




The address of the meeting is as follows:

    School of Computer Science
    University of Nottingham
    Jubilee Campus
    Wollaton Road
    Nottingham, NG8 1BB
    United Kingdom

Google Maps, coordinates: 52.953489, -1.187355.


The currency is the British Pound (GBP or £), nowadays very cheap. Debit/credit cards are accepted almost everywhere. In some situations, a small charge will be applied if you pay minor sums like £5 by card, and some small businesses (street food etc) may not accept cards. There is an ATM close to the School of Computer Science, but I suspect it chargers horrendous exchange fees.

Travel to Nottingham by Plane


  • East Midlands Airport (EMA): A small airport, and chances are that you won't find any suitable flights. If you do, you can take the Skylink bus to Nottingham city centre, or directly go by taxi to your hotel for ~30 GBP.
  • Birmingham (BHX): From the airport, you can get to Nottingham in around 1:40 by train. Usually, a single change at Birmingham New Street is sufficient.
  • Manchester (MAN): To Nottingham, it takes around 2:20 by train. Most connections only require a single change at Manchester Piccadilly.
  • Stansted (STN) and other London airports: Not recommended, but still okay if there is nothing better and if you choose the right route. From STN, you can get to Nottingham in 3 hours with only one change in Ely or Leicester. Avoid connections through London, those will be more expensive, require more changes, and are generally more stressful!

From the train station: either go by taxi (~7 GBP) or walk to Victoria Centre, from where you can take the bus lines 28 and 30 to Jubilee Campus.


The P&J hotel is in good location and has previously been used for meetings in Nottingham. Unfortunately, campus accommodation is NOT available, sorry. and similar websites work well in Nottingham. Living in the city centre is an option. The School of Computer Science is on Jubilee Campus, reachable from the city centre in 40 minutes (walking time) or ~15 minutes (bus 28 or 30 + walking).