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.

Wednesday, 11 Sep
09:30Welcome & coffee
10:00Introduction: code sprint proposals, planning
11:00Shaun Steenkamp: A use case for sized types
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
18:00Wrap-up meeting (summary)
Thursday, 12 Sep
09:30Holger Borum: Future Management Action Language
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
17:45Wrap-up meeting (summary)
Friday, 13 Sep
09:30Jesper Cockx: Reclaiming the power of computation (a manifesto)
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
17:30Wrap-up meeting (summary)
19:00Meeting dinner at Augustiner-Keller
Saturday, 14 Sep
09:30Shaun Steenkamp: Pattern matching for quotient types
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
17:30Wrap-up meeting (summary)
Sunday, 15 Sep Excursion
09:00Meet at the ticket machine near Platform 32 at Hauptbahnhof
09:24Train (BOB 87031) to Schliersee
10:22Walk to Tegernsee
??:22/52Train back to Munich
Monday, 16 Sep
09:30Thorsten Altenkirch: Higher coinductive types
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
17:30Wrap-up meeting (summary)
Tuesday, 17 Sep
09:30Wen Kokke: Programming Programming Language Foundations in Agda in Agda
10:30Coffee break
11:00Groups/Code sprints/Discussions
12:00Lunch
13:00Groups/Code sprints/Discussions
15:30Coffee break
16:30Groups/Code sprints/Discussions
17:30Wrap-up meeting

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
We present a construction of initial algebras for (strictly positive) equational systems using quotient types, mutual inductive-inductive definitions, and sized types. These initial algebras are a generalisation of W-types which cover many cases of QIT (or 1-HIT), including infinitely branching unordered trees, Blass-Lumsdaine-Shulman uncountable regular cardinals, and Swan's W-types with reductions. We needed to use sized types to show that the universal property is terminating. It is not clear that we could have done it with well-founded recursion.
(For the notion of an equational system, see §3 of: M Fiore & C-K Hur, "On the Construction of Free Algebras for Equational systems", TCS 410(2009)1704-1729.)
  • Holger Borum: Future Management Action Language
  • Jesper Cockx: Abstraction and computation (a manifesto) (slides)
  • Shaun Steenkamp: Pattern matching for quotient types
We present examples of eliminator syntax for postulated quotient types, and propose a pattern-matching syntax that improves readability and development speed, as well as avoiding problems inferring implicit arguments.
  • Thorsten Altenkirch: Higher coinductive types
  • Wen Kokke : Programming Programming Language Foundations in Agda in Agda
The foundation of how we think and reason about programming languages is import; how we teach those foundations is just as important. Programming Language Foundations in Agda (PLFA) is a new introductory textbook covering PL foundations in Agda, one of the more popular dependently typed programming languages. The book is presented as a literate programme and is freely accessible at plfa.inf.ed.ac.uk.

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:

Accommodation

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

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.