The twentieth edition of the Agda Implementors’ Meeting: Theory, implementation, and applications of Agda.
AIM XX will be held in Tallinn 16–22 October 2014 (Thu to Wed). Everyone with a genuine interest in Agda is invited to attend. 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.
We have reserved a room in the Academy of Sciences Building. The Academy is situated in the upper part of Tallinn’s beautiful and historic old town (Estonian Academy of Sciences, Kohtu 6, 10130 Tallinn).
We recommend that you stay in a hotel in or nearby the old town. Suggestions (in no particular order): L’Ermitage, Meriton Old Town Garden and Old Town, Bern, Taanilinna, St. Petersbourg, Meriton Spa.
Tallinn airport is only 4 km from the city centre. You can get a taxi (always check the price of taxis on the yellow sticker on the rear passenger window of the taxi) from the airport rank for <10 EUR to the city, or take a bus (no 2) to the centre for 1.6 EUR (tickets can be bought from the driver (who might not speak English unlike almost everybody else) with correct change).
- Rewrite rules for Agda
- framework for formal assurance case
- add your code sprint here
Minutes of Wrap up meeting
- James Chapman
- Wolfgang Jeltsch
- Niccolò Veltri
- Keiko Nakata
- Matteo Acerbi
- Jesper Cockx
- Andreas Abel
- Ulf Norell
- Andrea Vezzosi
- Nicolas Pouillard
- Tarmo Uustalu
- Silvio Capobianco
- Makoto Takeyama
- Guillaume Brunerie
- Sergey Kazenyuk
- Francesco Mazzoli
- Guilhem Moulin
- Denis Firsov
|10.00||Andreas Abel - Introduction to Agda|
|11.00||Andreas Abel - Introduction to Agda (continued)|
|14.00||Andreas Abel - Bug fixing|
|09.00||Ulf Norell - New cool stuff|
|11.00||Keiko Nakata - Formalising the realisability model for type theory|
|09.00||Francesco Mazzoli - Type checking with metavariables, unification (slides)|
|14.00||Niccolò Veltri - Two set-based approaches to quotients in type theory|
|09.00||Guillaume Brunerie - Cubical homotopy type theory|
|14.00||Andreas Abel - discussion|
|09.00||Matteo Acerbi - Modular constructions in dependently typed languages|
|15.30||Finish (to allow people to catch flights)|
Excursion - Sunday 19 October
13.00 Brunch at Gourmet Coffee, L. Koidula 13A, 10125 Tallinn - Take tram 1 from Hobujaama to Kadriorg. 1.60 EUR, correct change essential! Google understands public transport in Tallinn, but you can also check http://soiduplaan.tallinn.ee/. For taxis I recommend Reval Takso (+372 6014600 +372 5264111) or Tulika (+372 6 120 000). It’s walkable, but a bit far from the old town and the weather is probably going to be bad. Please don’t be late!
Walk to Kumu art museum in Kadriorg park.
Workshop dinner - Monday 20 October
19.00 Kolm Sibulat, Telliskivi 2, 10611. Menu choices must be made by Sunday!
Registration is now closed.
Registration closes 2 October 2014. Please use our online system to register.
The lunches during the meeting days 16–18 and 20–22 October and the workshop dinner 20 October cost 150 EUR.
Contact the organizers at email@example.com for further information.