Agda Implementors' Meeting XXX

The thirtieth Agda Implementors' Meeting will take place in Munich, Germany from 2019-09-11 to 2019-09-17 (Wednesday to Tuesday). 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.

Important dates

2019-08-31

Registration deadline (soft)

2019-09-11 (Wed) to 2019-09-17 (Tue)

AIM XXX

Programme

All talks, coffee breaks and sprints take place in room B349 of the LMU Department of Mathematics.

Talks

• Shaun Steenkamp: A use case for sized types: Construction of initial algebras for Fiore-Hur equational systems using sized types, with applications to quotient inductive types

• Holger Borum: Future Management Action Language
• Jesper Cockx: Abstraction and computation (a manifesto) (slides)
• Shaun Steenkamp: Pattern matching for quotient types

• Thorsten Altenkirch: Higher coinductive types
• Wen Kokke : Programming Programming Language Foundations in Agda in Agda

Code sprint suggestions

• Thorsten Altenkirch:
  1. Implement constructor (and maybe destructor) to allow arbitrary sequence of constructors (and destructors), Relevant issue
  2. Implementing higher coinductive types in cubical agda,
  3. Implement 2-level cubical type theory
• Jesper Cockx: cumulativity
• Guillaume Allais: With on steroids
• Martin Molzer: A real number implementation as a coinductive digit stream
• James Wood & Wen Kokke: Linear Algebra
• Evgenii: fix open issues
• Fredrik, Ulf: work on the reflection machinery
• Andreas: inference for erasure

Participants

• Andreas Abel
• Stephan Adelsberger
• Evgenii Akentev
• Guillaume Allais
• Thorsten Altenkirch
• Malin Altenmüller
• Holger Borum
• Jesper Cockx
• Alexandre Delanoe
• Frederic Jouault
• Gabor Greif
• Wen Kokke
• Nils Köpp
• Connor Leahy
• John Leo
• Fredrik Nordvall Forsberg
• Ulf Norell
• Martin Molzer
• Nicolas Pouillard
• Jakob von Raumer
• Stephan Sahm
• Shaun Steenkamp
• James Wood
• Chuangjie Xu
• ... your name could be here :)

Location

The meeting will take place in Room B349 of our institute:

    Mathematisches Institut
    Ludwig-Maximilians-Universität München
    Theresienstr. 39
    80333 Munich
    Germany

Room B349 is on the third floor of the "middle" B building. You can enter any of the buildings from either side, then take the lift from the B building.

• If you arrive by air at Munich Airport, the easiest way into the city is by the S-Bahn, the regional railway system. Take S-Bahn Line S1 or S8 (suburban trains) to Karlsplatz (Stachus). Then take Tram 27 (direction of Petuelring) or 28 (direction of Scheidplatz) to the tram stop Pinakotheken, which takes about 5 minutes (3 stops). The Math Institute is in the building right next to the tram stop. Tickets must be purchased at the ticket machines (ground floor near the escalators to the S-Bahn station in the airport). If you travel alone, you might want to buy an adult single day ticket (all zones) - if you are a group of two or more (up to five), you should buy an adult group ticket (all zones). Tickets must be validated (stamped) before entering the trains. In total the journey takes about 1 hour.
• If you get to Munich by train, you can choose to buy either a single ride ticket, a day ticket, or a group day ticket (for groups up to five) - or even three-day versions of these. The Math Institute is located in the inner district, so "Innenraum" tickets are sufficient for getting from the central train station (Hauptbahnhof) to the Math Institute. You can take Bus 58 or 100, both leaving from the bus stop at the northern exit of the central train station (Hauptbahnhof Nord), to the bus stop Pinakotheken, which takes about 7 minutes (4 stops). Walk along Barer Straße to the north for 3 minutes. Then you will reach the building of the Math Institute.

Excursion

The excursion will be a walk from Schliersee to Tegernsee on Sunday 15th September. The distance is about 14 km, with a climb of 600 m, on good paths. Please bring comfortable shoes (e.g. hiking boots or running shoes). There are several huts to stop at for refreshments on the way. We will meet at the ticket machine near Platform 32 at Hauptbahnhof and buy tickets together (around 7.5 EUR per person, day ticket).

About Munich

The official website of the city of Munich is https://www.muenchen.de/, where you can find information about the cultural life in Munich and a link to the tourist information. Here are some more links that might be useful:

• the Munich tourist office,
• the official hotel booking service of the Munich tourist office,
• general information about finding your way around Munich on the international website of the MVV (linked transport system around Munich) and on the Transport Portal, and
• Munich sights, some suggestions (in German).

Accommodation

The following accommodations provide special conditions for LMU. Please refer to these when booking via telephone or e-mail.

• Hotel Antares, Amalienstraße 20, 80333 München
• Das Hotel, Türkenstr. 35, 80799 München
• Frederics Apartments, Hohenzollernplatz 7, 80796 München
• Pension Isabella, Isabellastr. 35, 80796 München

Registration

You can register for the meeting by filling out the form below and emailing it to Chuangjie Xu.

There is no registration fee. Coffee breaks would be included. Transportation, accommodation and meals are to be covered by the participant.

    Registration form for Agda Implementors' Meeting XXX

    Name:

    Title and optionally abstract (if you want to give a talk or lead a discussion):

    Suggestions for code sprints (optional):

    Additional comments:

Sponsorship

This meeting is supported by the LMUexcellent Junior Researcher Fund.