AIMXX

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.00AIMXX Planning
10.00Andreas Abel - Introduction to Agda
10.30Coffee
11.00Andreas Abel - Introduction to Agda (continued)
12.30Lunch (provided)
14.00Andreas Abel - Bug fixing
15.30Coffee
16.00Hacking
17.30Wrap-up
18.00Finish
Fri 17
09.00Ulf Norell - New cool stuff
10.30Coffee
11.00Keiko Nakata - Formalising the realisability model for type theory
12.30Lunch (provided)
14.00Hacking
15.30Coffee
16.00Hacking
17.30Wrap-up
18.00Finish
Sat 18
09.00Francesco Mazzoli - Type checking with metavariables, unification (slides)
10.30Coffee
11.00Hacking
12.30Lunch (provided)
14.00Hacking
15.30Coffee
16.00Hacking
17.30Wrap-up
18.00Finish
Mon 20
09.00Hacking
10.30Coffee
11.00Hacking
12.30Lunch (provided)
14.00Niccolò Veltri - Two set-based approaches to quotients in type theory
15.30Coffee
16.00Hacking
17.30Wrap-up
18.00Finish
Tue 21
09.00Guillaume Brunerie - Cubical homotopy type theory
10.30Coffee
11.00Hacking
12.30Lunch (provided)
14.00Andreas Abel - discussion
15.30Coffee
16.00Hacking
17.30Wrap-up
18.00Finish
Wed 22
09.00Matteo Acerbi - Modular constructions in dependently typed languages
10.30Coffee
11.00Hacking
12.30Lunch (provided)
14.00Wrap-up
15.00Coffee
15.30Finish (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.