Agda Implementors' Meeting XXXI

The thirty-first Agda Implementors' Meeting will take place in Edinburgh from 2020-04-01 to 2020-04-07 (Wednesday to Tuesday). The meeting will be similar to previous ones:

  • Presentations concerning theory, implementation, and use cases of Agda.
  • Discussions around issues of the Agda language.
  • Plenty of time to work on or in Agda, in collaboration with the other participants.

Important dates

Registration deadline (soft)
2020-04-01 (Wed) to 2020-04-07 (Tue)



All talks, coffee breaks and sprints take place rooms 5.02 of the Bayes Centre, University of Edinburgh.

Wednesday, 1 April 
Thursday, 2 April
Friday, 3 April
Saturday, 4 April
Sunday, 5 April
Monday, 6 April
Tuesday, 7 April


  • John Leo: Music Tools
    An update on the progress of tools written in Agda for the analysis and synthesis of music. Joint work with Youyou Cong.
  • (your talk here)

Code sprint suggestions

  • Wen Kokke: Integration with SAT and SMT solvers
    For their Ph.D., Karim Kanso wrote a quite general framework for integrating Agda with SAT and SMT solvers. It would be a shame to let this code bitrot away, especially when integration with SMT solvers is such a useful tool! I propose that we asses how much effort a merge of this code into the master branch would be. (Help wanted.)
  • (your code sprint here)


  • Wen Kokke
  • Orestis Melkonian
  • John Leo
  • (your name here)


The meeting will take place in Room 5.02 of the ICMS:

Bayes Centre, The University of Edinburgh
47 Potterrow
Edinburgh EH8 9BT

The ICMS is located at the top floor of the Bayes Centre. You can enter the building via the main doors. The building is access controlled, so you will have to sign in at the reception. Take the elevator to the fifth floor, and the ICMS will be to your right. For more detailed information, see the ICMS website.


More information will appear here.

About Edinburgh

Edinburgh is Scotland's compact, hilly capital. It has a medieval Old Town and elegant Georgian New Town with gardens and neoclassical buildings. Looming over the city is Edinburgh Castle, home to Scotlandís crown jewels and the Stone of Destiny, used in the coronation of Scottish rulers. Arthurís Seat is an imposing peak in Holyrood Park with sweeping views, and Calton Hill is topped with monuments and memorials.

More information will appear here.


The ICMS offers a number of suggestions for hotels nearby:

  • Edinburgh First
    Edinburgh First is the accommodation service of the University of Edinburgh and they offer good quality, well priced rooms at a number of locations in the City year round. If you book your accomodation via Edinburgh First, you can use the discount code 'EVENT' to receive a 15% discount.
  • IBIS South Bridge
    This IBIS hotel is located five-minutes walk from ICMS. There is another IBIS at Hunter Square which is a little further away towards the city centre.
  • 10 Hill Place
    This hotel is located two minutes from ICMS.
  • Jury's Inn
    Jury's Inn is a ten-minute walk from ICMS and benefits from being very close to the railway station and the airport bus bus stop.
  • Leonardo Boutique Hotel Edinburgh City
    This hotel is located on Lauriston Place and is a ten-minute walk from ICMS.
  • Premier Inn
    This chain has a number of hotels close to ICMS, including Princes Street, East Market Street and Lauriston Place.
  • Princes St Backpackers
    If you require budget accomodation, Princes St Backpackers is one of the most affordable hostels, and is about 20 minutes walk from the ICMS.
    (Note: This location was added by the organisers, and isn't recommended by the ICMS.)


You can register for the meeting by filling out the form below and emailing it to Wen Kokke.

There is no registration fee. Coffee breaks would be included. Transportation, accommodation and meals are to be covered by the participant.

    Registration form for Agda Implementors' Meeting XXXI


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

    Suggestions for code sprints (optional):

    Additional comments: