Date/Time
Date(s) - 10/11/2022 - 16/11/2022
9:30 am - 4:30 pm
Location
University of Edinburgh
The 31st Agda Implementors’ Meeting will take place in Edinburgh, Scotland from Thursday 10 November 2022 to Wednesday 16 November 2022. Note that AIMXXXI was initially planned for 2019 but got postponed due to COVID-19, whilst we had several online meetings XXXII-XXXV. The meeting will consist of:
- Presentations concerning theory, implementation, and use cases of Agda and other Agda-like languages.
- Discussions around issues related to the Agda language.
- Plenty of time to work in, on, under or around Agda, in collaboration with other participants.
Important dates
- Registration deadline: 10.10.2022
- AIM XXXI: 10.11.2022 (Thu) to 16.11.2022 (Wed)
Programme
All talks, coffee breaks and sprints take place on the ground floor of the Informatics Forum of the University of Edinburgh.
Thursday, 10 November (Room G.03)
- 09:30 Talk: TBA
- 10:30 Coffee break
- 11:00 Groups/Code sprints/Discussions
- 12:00 Lunch
- 13:00 Groups/Code sprints/Discussions
- 14:00 Coffee break
- 15:00 Groups/Code sprints/Discussions
- 16:00 Wrap-up meeting (summary)
Friday, 11 November (Room G.07)
- 09:30 Talk: TBA
- 10:30 Coffee break
- 11:00 Groups/Code sprints/Discussions
- 12:00 Lunch
- 13:00 Groups/Code sprints/Discussions
- 14:00 Coffee break
- 15:00 Groups/Code sprints/Discussions
- 16:00 Wrap-up meeting (summary)
Sunday, 13 November (Excursion)
- 09:00-19:00 Hike to North Berwick, c.f. this section
Monday, 14 November (Room G.03)
- 09:30 Talk: TBA
- 10:30 Coffee break
- 11:00 Groups/Code sprints/Discussions
- 12:00 Lunch
- 13:00 Groups/Code sprints/Discussions
- 14:00 Coffee break
- 15:00 Groups/Code sprints/Discussions
- 16:00 Wrap-up meeting (summary)
Tuesday, 15 November (Room G.07)
- 09:30 Talk: TBA
- 10:30 Coffee break
- 11:00 Groups/Code sprints/Discussions
- 12:00 Lunch
- 13:00 Groups/Code sprints/Discussions
- 14:00 Coffee break
- 15:00 Groups/Code sprints/Discussions
- 16:00 Wrap-up meeting (summary)
Wednesday, 16 November (Room G.07)
- 09:30 Talk: TBA
- 10:30 Coffee break
- 11:00 Groups/Code sprints/Discussions
- 12:00 Lunch
- 13:00 Groups/Code sprints/Discussions
- 14:00 Coffee break
- 15:00 Groups/Code sprints/Discussions
- 16:00 Wrap-up meeting (summary)
Talks
- Andreas Nuyts: State of cubical agda and its library (Discussion): Working with constraints; Equality-in-equality-out category theory
- Philip Wadler: Update on PLFA
- John Leo: Counterpoint Analysis and Synthesis. Update on the status of this project since the FARM 2022 presentation.
- Patrik Jansson: Extensional equality preservation as a traversal
- Antoine Van Muylder: Extending cubical Agda with Internal Parametricity
Code sprint suggestions
- Andreas Nuyts: Equality-in-equality-out category theory in agda-cubical
- John Leo: work on MusicTools; potential integration with Schmitty
- (your code sprint here)
Participants
- Orestis Melkonian
- James Chapman
- Jesper Cockx
- Andreas Nuyts
- Philip Wadler
- John Leo
- Fredrik Nordvall Forsberg
- Patrik Jansson
- Joris Ceulemans
- Antoine Van Muylder
- (your name here)
Location
The meeting will take place in the ground floor of the Informatics Forum:
Informatics Forum, The University of Edinburgh
10 Crichton St
Edinburgh EH8 9AB
Scotland
The rooms are located in the ground floor, just after you enter the building via the main doors. The building is access controlled, so you will have to sign in at the reception.
