The fifteenth edition of the Agda Implementors’ Meeting: Theory, implementation, and applications of Agda.
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.
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).
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
- Andreas Abel, A Semantics for Agda’s Mixed Inductive-Coinductive types
- Thorsten Altenkirch, Eliminating Data
- James Chapman, Agda tutorial
- Frederic Kettelhoit, Towards a Prelude for Agda
- Yoshiki Kinoshita, Category-Theoretical Investigation of Setoids
- Bengt Nordström, A Formalistic Type Theory
Discussions and Code Sprint Suggestions
- 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
- James, Write a manual by raiding the release notes
- 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 Ski! 12:00 Meet at Berggasthof Walleralm (probably) for lunch Ski! 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 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).
- Sudelfeld map is where we ski on Thursday.
- 4,40 EUR for BOB return trip Fischbachau-Bayrischzell
- 28 EUR for day pass
- 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 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 bahn.de. 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.
- 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.
- 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 bahn.de 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.
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:
Name: Affiliation: email: Accomodation * Date of arrival: * Date of departure: Excursion: * Alpine skiing (yes/no): * Nordic skiing (yes/no): Program: * I'd like to give a talk or lead a discussion (yes/no): Title: Abstract: (optional) * Suggestion for code-sprint (optional):