The fifteenth edition of the Agda Implementors' Meeting: Theory, implementation, and applications of Agda.
Venue
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
info@aurachhof.de
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
Program
(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
Talks
- 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
CodeSprints
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"
Participants
- 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
Excursion
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
Leisure
- 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:
- Aibski is directly in the ski resort (Full equipment: 34 EUR/day).
- Skischule Sudelfeld is a bit cheaper (24 EUR/day) but not where the slopes are map.
- Sportalm Bayrischzell seems to have rental at the slopes for 26 EUR/day.
- 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).
Travel
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.
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 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.
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.
Registration
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):