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.
Venue
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).
Accommodation
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.
Travel
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).
Code sprints
- Rewrite rules for Agda
- framework for formal assurance case
- add your code sprint here
Minutes of Wrap up meeting
Participants
- 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
Programme
| Thu 16 | |
|---|---|
| 09.00 | AIMXX Planning |
| 10.00 | Andreas Abel - Introduction to Agda |
| 10.30 | Coffee |
| 11.00 | Andreas Abel - Introduction to Agda (continued) |
| 12.30 | Lunch (provided) |
| 14.00 | Andreas Abel - Bug fixing |
| 15.30 | Coffee |
| 16.00 | Hacking |
| 17.30 | Wrap-up |
| 18.00 | Finish |
| Fri 17 | |
| 09.00 | Ulf Norell - New cool stuff |
| 10.30 | Coffee |
| 11.00 | Keiko Nakata - Formalising the realisability model for type theory |
| 12.30 | Lunch (provided) |
| 14.00 | Hacking |
| 15.30 | Coffee |
| 16.00 | Hacking |
| 17.30 | Wrap-up |
| 18.00 | Finish |
| Sat 18 | |
| 09.00 | Francesco Mazzoli - Type checking with metavariables, unification (slides) |
| 10.30 | Coffee |
| 11.00 | Hacking |
| 12.30 | Lunch (provided) |
| 14.00 | Hacking |
| 15.30 | Coffee |
| 16.00 | Hacking |
| 17.30 | Wrap-up |
| 18.00 | Finish |
| Mon 20 | |
| 09.00 | Hacking |
| 10.30 | Coffee |
| 11.00 | Hacking |
| 12.30 | Lunch (provided) |
| 14.00 | Niccolò Veltri - Two set-based approaches to quotients in type theory |
| 15.30 | Coffee |
| 16.00 | Hacking |
| 17.30 | Wrap-up |
| 18.00 | Finish |
| Tue 21 | |
| 09.00 | Guillaume Brunerie - Cubical homotopy type theory |
| 10.30 | Coffee |
| 11.00 | Hacking |
| 12.30 | Lunch (provided) |
| 14.00 | Andreas Abel - discussion |
| 15.30 | Coffee |
| 16.00 | Hacking |
| 17.30 | Wrap-up |
| 18.00 | Finish |
| Wed 22 | |
| 09.00 | Matteo Acerbi - Modular constructions in dependently typed languages |
| 10.30 | Coffee |
| 11.00 | Hacking |
| 12.30 | Lunch (provided) |
| 14.00 | Wrap-up |
| 15.00 | Coffee |
| 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.
17.00 Jazzkaar concert with Miamee at Kumu. Feel free to book tickets in advance, I am hoping that we can book tickets when we arrive at Kumu, but this is not certain. Miamee at Spotify
Workshop dinner - Monday 20 October
19.00 Kolm Sibulat, Telliskivi 2, 10611. Menu choices must be made by Sunday!
Registration
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.
Host
Institute of Cybernetics at TUT
Sponsor
AIM XX is supported by the European Regional Development Fund funded Estonian ICT project Coinduction.
Contact
Contact the organizers at aimxx@cs.ioc.ee for further information.