The twenty-second Agda Implementors' Meeting will take place in Leuven 2015-09-16 to 2015-09-22 (Wed to Tue). 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.
Location
The meeting will take place on campus Arenberg in building 200S, around 2,5 km from the center of Leuven. The building is in between two larger ones (L and M). The entrance is hidden somewhat behind a hedge and a bike shed (see OpenStreetMaps).
Coffee breaks will be provided, as well as WIFI through eduroam. Lunch is available at De Moete (sandwiches and soup) or Alma III (warm meals).
From the central train station, you can go to campus Arenberg by bus. Bus 616 takes you there in about 15 minutes, number 2 does the same in 27 minutes. You can also go by bike, which takes 10-15 minutes. See below for information on renting a bike.
Excursion
On Sunday (20/8), there will be a guided walk through the historical center of Leuven. We will meet at noon at the Ladeuzeplein (at the university library) for lunch in De Appel. At 2 p.m., the guide will meet us at de Grote Markt. After the tour, we could go for some drinks in The Capital (selection of over 2000 Belgian beers).
Dinner
On Monday (21/8), there will be a conference dinner at Bistro Lust (http://www.bistrolust.be). We have a reservation at 7:30 p.m.
Daily Schedule
09:30 - 11:00 Session 1: Talks & Tutorials 10:45 - 11:15 Coffee 11:00 - 12:30 Session 2: Talks & Discussions 12:30 - 13:30 Lunch 13:30 - 15:00 Session 3: Code Sprints 15:00 - 15:30 Coffee 15:30 - 17:30 Session 4: Code Sprints 17:30 - 18:00 Wrap-up meeting: Results, Demos
Preliminary program
Wed, September 16 09:30 Welcome 10:00 Nils Anders Danielsson: Higher and/or dependent lenses 10:45 Coffee 11:15 Discussions / code sprints 12:30 Lunch 13:30 Code sprints 15:00 Coffee 15:30 Code sprints Thu, September 17 09:30 Philipp Hausmann: The Agda UHC backend 10:15 Wolfram Kahl: Towards Verified Graph Transformation as Basis for Code Generation 10:45 Coffee 11:15 Discussions / code sprints 12:30 Lunch 13:30 Code sprints 15:00 Coffee 15:30 Code sprints Fri, September 18 09:30 Ulf Norell: Escaping from record hell 10:45 Coffee 11:15 Discussions / code sprints 12:30 Lunch 13:30 Code sprints 15:00 Coffee 15:30 Code sprints Sat, September 19 10:00 Andreas Nuyts: Directed homotopy type theory with an enhanced variance system 10:45 Coffee 11:15 Happy hacking! 12:30 Lunch 15:00 Coffee Sun, September 20 12:00 Lunch at De Appel 14:00 guided walk through Leuven's historical center Mon, September 21 09:30 Thomas Winant and Jesper Cockx: STAMP: Strongly Type-sAfe Meta-Programming for Haskell in Agda 10:45 Coffee 11:15 Discussions / code sprints 12:30 Lunch 13:30 Code sprints 15:00 Coffee 15:30 Code sprints 19:30 Conference dinner at Bistro Lust Tue, September 22 09:30 Happy hacking!
Travel to Leuven
- By plane: from Brussels airport, you can reach Leuven by train in about 15 minutes.
- By train: most international trains stop at Brussels South (Bruxelles Midi), from where the intercity train takes you to Leuven in about 30 minutes. Further information about train service in Belgium can be found at https://www.belgianrail.be/en.
Getting around in Leuven
Leuven isn't very big, so it's easy to get around.
- By bus: Bus service is handled by De Lijn (https://www.delijn.be/en/). You can buy tickets at the Lijnwinkel, located next to the station (on your right).
- By bike: You'll notice that most people in Leuven go everywhere by bike. You can rent a bike for a week for 24 euro at the Bike Point (http://www.kuleuven.be/velo/fietspunteng.html), which is also located next to the train station (on your left).
Accommodation
- The Lodge (0.8 km by foot)
- Boardhouse hotel (1.3 km by foot)
- Begijnhof hotel (1.8 km by foot)
- Hotel New Damshire (17 minutes by bus)
- Condo Gardens (10-20 minutes by bus)
- Ibis budget (15-27 minutes by bus)
- ...
Registration
Officially, registration is now closed. If you wish to attend and haven't registered yet, please contact the organizers by sending a mail to jesper [DOT] cockx [AT] cs [DOT] kuleuven [DOT] be.
Participants
Andreas Abel, University of Gothenburg
Stephan Adelsberger, WU Wien
Guillaume Allais, University of Strathclyde
James Chapman, University of Strathclyde
Jesper Cockx, KU Leuven (organizer)
Nils Anders Danielsson, University of Gothenburg
Dominique Devriese, KU Leuven (co-organizer)
Philipp Hausmann, Universiteit Utrecht
Víctor López Juan, Chalmers University
Wolfram Kahl, McMaster University (from Sept. 17)
Steven Keuchel, Universiteit Gent
Sergey Kotikov
Fredrik Nordvall Forsberg, University of Strathclyde
Ulf Norell, University of Gothenburg
Andreas Nuyts, KU Leuven
Paolo Torrini, KU Leuven
Andrea Vezzosi, Chalmers University
Talks
Wolfram Kahl: ``Mouldable Code'' for Correct-by-Construction SW Needs Nested Theories
Ulf Norell: Escaping from record hell
Philipp Hausmann: The Agda UHC backend (slides)
Nils Anders Danielsson: Higher and/or dependent lenses
Andreas Nuyts: Directed homotopy type theory with an enhanced variance system
Jesper Cockx Thomas Winant: STAMP: Strongly Type-sAfe Meta-Programming for Haskell in Agda (slides)
Pre-meeting Code Sprint Proposals
Wolfram Kahl: Make --sharing work
Wolfram Kahl: Get sharing into the back-ends
Philipp Hausmann: Port some optimizations to MAlonzo / UHC from Epic
Philipp Hausmann: New FFI for Agda
Jesper Cockx: Records with individually level-polymorphic fields (see http://homotopytypetheory.org/2015/07/05/modules-for-modalities/)
Jesper Cockx: Thinking about shape-irrelevance
Ulf Norell: Improving efficiency of scope checking
Nils Anders Danielsson: Blocking instead of abstract