The fifteenth edition of the Agda Implementors' Meeting: Theory, implementation, and applications of Agda.

Thorsten's facebook album


AIM XV takes place 19-26 February 2012 at Hotel Aurachhof in Fischbachau near Munich, situated beautifully in a hilly landscape in reach of the Alps. The hotel offers accommodation, full board, and meeting rooms, at the price of EUR 85/person/day. The price for the full meeting is 595 EUR. The daily fee (lunch and coffee) is 22 EUR.

Hotel Aurachhof
Bahnhofstraße 4
D-83730 Fischbachau
Tel. +49-8028-903-0
Fax +49-8028-903-199

The week of AIM XV is school holiday in Bavaria. It is Fasching (carneval), the season before beginning of lent. People dress in costumes and celebrate on the streets (more so in the Rhein area of Germany). Tuesday, 22. is Faschingsdienstag, shops and offices usually close at noon, in the afternoon people celebrate the end of carneval, before lent begins on Wednesday (Aschermittwoch).

Daily Schedule

For day participants: A BOB train leaves Munich Hauptbahnhof at 8:10 and arrives in Fischbachau at 9:17, on time for the morning session. Trains back to Munich hourly at :45, e.g. 18:45.

07:30 - 09:30 Breakfast
09:30 - 11:00   Session 1: Talks & Tutorials
11:00 - 11:15 Coffee
11:15 - 12:00   Session 2: Talks & Discussions
12:00 - 13:00 Lunch
13:00 - 14:00 Break
14:00 - 15:30   Session 3: Code Sprints
15:30 - 16:00 Coffee
16:00 - 18:30   Session 4: Code Sprints
18:30 - 19:00   Wrap-up meeting: Results, Demos 
19:00 - 20:00 Dinner
20:00 -       Leisure time


(not etched in stone)

Su, 19 Feb: Arrival

Mo, 20 Feb: 09:30 Opening
            09:45 James Chapman, Agda tutorial I: Dependent types, proof editing and all that
            11:15 Frederic Kettelhoit: Towards a prelude for Agda
            14:00 Code sprint proposals and allocation
            14:45 Happy hacking!

Tu, 21 Feb: 09:30 James Chapman, Agda tutorial II: Real world Agda programming
            10:15 Yoshiki Kinoshita, Category-theoretical investigation of setoids
            11:15 Thorsten Altenkirch, Eliminating Data

We, 22 Feb: 09:30 Andreas Abel, A semantics for Agda's mixed inductive-coinductive types
            11:15 Bengt Nordström, A formalistic type theory

Th, 23 Feb: Excursion

Fr, 24 Feb: Discussions and code-sprints

Sa, 25 Feb: Discussions and code-sprints; wrap-up meeting

Su, 26 Feb: Departure



Discussions and Code Sprint Suggestions

Hacking Agda

  • Andreas, Pattern-matching definitions of functions with varying arity
  • Andreas, Strengthening Dominique's instance inference
  • Thorsten, Smart case
  • James, Destructor patterns
  • Makoto, Agda internal: preserving and printing back let-expressions

Documenting Agda

  • James, Write a manual by raiding the release notes

Using Agda

  • Yoshiki, Coding Catoids
  • Makoto, Relating the way formal theories are revised with "argumentation"


  • Andreas Abel
  • Stephan Adelsberger
  • Thorsten Altenkirch
  • James Chapman
  • Nils Anders Danielsson
  • Dominique Devriese
  • Peter Divanszky
  • Peter Dybjer
  • Ambrus Kaposi
  • Frederic Kettelhoit
  • Steven Keuchel
  • Yoshiki Kinoshita
  • Ramana Kumar
  • Andres Löh
  • Guilhem Moulin
  • Bengt Nordström
  • Makoto Takeyama
  • Paul van der Walt


An excursion will take place on Thursday, 23. The hotel provides packed lunch. We will split into three groups:

  • Alpine skiing: Andreas, Stephan, Thorsten (46), James (44), Peter Divanszky (41), Ambrus (42), Yoshiki (43), Guilhem
09:00 Meet in hotel lobby; go to station, buy tickets
09:17 BOB train to Bayrischzell (arrives 09:28)
      Those who need to rent ski go by car
09:30 Bus from Bayrischzell to Schwebelift
09:42 Arrive Unteres Sudelfeld
12:00 Meet at Berggasthof Walleralm (probably) for lunch
16:05 Meet at Unteres Sudelfeld 
16:15 Bus leaves at Unteres Sudelfeld to Bayrischzell (arrives 16:30)
16:35 BOB train to Fischbachau (arrives 16:45)
  • Nordic skiing: Nisse, Dominique, Ramana (43), Bengt
09:00 Meet in hotel lobby; go to station, buy tickets
09:17 BOB train to Bayrischzell (arrives 09:28)
09:30 Walk to Sportalm Bayrischzell, Alpenstr. 70 (or take bus at 9:56); rent ski
(16:02 Bus line "Langlauf" arrives at Bayrischzell Bahnhof) 
16:30 Back at Bayrischzell Bahnhof
16:35 BOB train to Fischbachau
  • Not participating / already left: Peter Dybjer, Frederic, Steven, Makoto, Paul


  • Bowling (dt. Kegeln) in the Hotel: 10 EUR/person/evening.
  • Sauna in the Hotel: 10 EUR/person/evening.
  • Cafe Winkelstüberl (map) near Fischbachau is locally famous for its big slices of Kuchen (cake). A 3.4 km walk from Hotel Aurachhof, on weekdays there is an infrequent bus (9552) Fischbachau Bahnhof - Winkl (Fischbachau).

Alpine Ski

  • Sudelfeld map is where we ski on Thursday.
  • Costs:
    • 4,40 EUR for BOB return trip Fischbachau-Bayrischzell
    • 28 EUR for day pass
  • Skirental:
  • Skibus Bayrischzell schedule
    • For Alpine skiing: Leaves from Bayrischzell Bahnhof 8:30, 9:30, 10:30, 11:30 and returns there 15:30 and 16:30. Takes 5 min to Schwebelift (goes up to rental) and 12-15 min to Unteres Sudelfeld.
    • For Nordic skiing: Leaves from Bayrischzell Bahnhof 9:56, 10:56 and returns there 14:46 and 16:02. Takes 2 min to Sportalm (rental) and 11 min to farthest stop (Bäckeralm).

Nordic Ski

  • Nordic skiing tracks in Fischbachau.
  • Nordic ski rental (dt. Langlauf) in shop Hautmann. Open Tue-Fr afternoon (13.30-18.00) and Sat morning (9.00-12.00).


To plan train trips in Germany (or should I say Europe?), I recommend Helpful search values could be: From: Airport Munich To: Fischbachau Bahnhof.

Reach Munich Hauptbahnhof by train if you are at a reasonable distance (a TGV runs from Paris in 6 hours).

From Munich Airport (MUC) Franz-Josef-Strauß, take S-trains S1 or S8 to Munich Hauptbahnhof. Allow 1 hour for the trip.

From Munich Hauptbahnhof, take special train BOB (Bayerische Oberlandbahn) to Bayrischzell and exit at Fischbachau. The trip takes a bit over an hour.

From Fischbachau Bahnhof it is a 200m walk to the hotel.

Please note:

  • BOB Timetable: AIM XV takes place during school holidays (Ferien), the trains under column Schule won't run.
  • The BOB train leaves from Flügelbahnhof Nord (tracks 27-36), see Munich station map, upper left corner.
  • The BOB train usually splits in Holzkirchen; make sure you are in the part that goes to Bayrischzell!
  • You can also enter the BOB train at S-train stop Donnersbergerbrücke. This way, you can avoid the busy and possibly confusing Munich Hauptbahnhof. If coming from MUC you want to change at Donnersbergerbrücke, take an S1 from MUC.

Train tickets

  • Full trip: MUC -> Fischbachau: Take Bayern-Single-Ticket for 21 EUR. It is valid on all local trains, including S-train and BOB. You can buy it at the Bahn counter at MUC or online at when you search for your connection there.
  • Partial trip: MUC -> Hauptbahnhof via S-train: You need a ticket for the MVV (Munich traffic association). You can buy a Streifenkarte (stripe card) for 12 EUR and cancel 8 stripes (9.60 EUR). Alternatively, get a Single-Tageskarte Gesamtnetz (single day ticket entire network) for 10.80 EUR. You get the ticket at the Bahn counter or a ticket vending machine. In any case, remember to cancel the ticket in the blue ticket stamp machine!
  • Partial trip: Hauptbahnhof -> Fischbachau: Tickets: A single ticket is 13,60 EUR. There are special BOB-vending machines.

Group tickets

If you are coming in a group, you can save by buying a partner ticket for a group up to 5 persons.

  • Full trip: MUC -> Fischbachau: Take Bayern-Ticket for 29 EUR.
  • Partial trip: MUC -> Hauptbahnhof: Take a Partnertageskarte Gesamtnetz (partner day ticket entire network) for 19.60 EUR.
  • Partial trip: Hauptbahnhof -> Fischbachau: buy a BOB-MVV-Ticket for 25 EUR.

Ask me for additional advice on travelling to AIM XV.


Official registration has closed. If you missed this deadline, but want to participate nevertheless, please send me email as soon as possible. Note: no separate booking of Hotel Aurachhof required, I take care of that when you register.

To register, please send an email to me (andreas dot abel at ifi dot lmu dot de), filling out the following form:


* Date of arrival:
* Date of departure:

* Alpine skiing (yes/no):
* Nordic skiing (yes/no):

* I'd like to give a talk or lead a discussion (yes/no):
Abstract: (optional)

* Suggestion for code-sprint (optional):

Page last modified on February 25, 2012, at 09:00 am
Powered by PmWiki