Agda Implementors' Meeting XXII

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

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