Agda Implementors' Meeting XXVI

The twenty-sixth Agda Implementors' Meeting has taken place in Budapest, Hungary from 2018-01-29 to 2018-02-03 (Mon to Sat). The meeting was 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

2018-01-28

Registration deadline (not strict).

2018-01-29 (Mon) to 2018-02-03 (Sat)

AIM XXVI

Registration

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

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

    Registration form
    Agda Implementors' Meeting XXVI

    Name:

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

    Suggestions for code sprints (optional):

    Additional comments:

Participants

• Andreas Abel
• Stephan Adelsberger
• Guillaume Allais
• Csanád Baksay
• Jesper Cockx
• Péter Diviánszky (local organiser)
• Peter Dybjer
• Gábor Greif
• Ambrus Kaposi (main local organiser, phone: +36 20 775 2939)
• András Kovács (local organiser)
• Balázs Kőműves (local organiser)
• John Leo
• Fredrik Nordvall Forsberg
• Ulf Norell
• Eric Prates
• Andrea Vezzosi

Daily Schedule

Talks

Presentations on theory, implementation, and use cases of Agda and type theory are welcome.

If you would like to present something, you can propose a talk either when you register, or, write an email to Ambrus.

• Stephan Adelsberger: On implementing GUIs in Agda
• Guillaume Allais: A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
• Jesper Cockx: Elaborating left-hand sides of definitions by pattern matching
• András Kovács: Sharing-Preserving Elaboration with Precisely Scoped Metavariables
• Fredrik Nordvall Forsberg: Quotient Inductive-Inductive Types
• Ambrus Kaposi: Higher Inductive-Inductive Types
• Péter Diviánszky: Type inference calculus

Detailed program

Code sprint suggestions

• AutoZero: a reimplementation of proof search (Andreas Abel)
• Fixing long import lists (Jesper)
• implicit coercions, bounded level polymorphism, dependent type providers (Guillaume)
• New option --omega-in-omega (Jesper)
• Forced constructor patterns (Jesper)

Code sprint presentation round:

Ambrus: Cubical type theory without intervals, prototype in Haskell

John: join AutoZero

Peter:
  - Tutorial: Agda for Logicians
    build up from basic stable features, add more
  - work on lecture notes

Andras: options for printing terms (in Goal buffer etc.)
  - e.g. suppress module/record parameters

Guillaume:
  - Warnings: turn "missing definitions" into a warning
  - Dependent type providers:
    * run IO actions at type checking time
    * e.g. can get database schemas as type definitions.

Fredrik:
  - Warning: scope checking warnings conflict with caching

Gabor: (Haskell hacker)
  - Can discuss performance problems with compilation etc.
  - Formalize higher categories (Ambrus is interested)

Balazs: (Haskell hacker, only part time participant)
  - join Peter or Gabor
  - implement dependent type checker

Frederic:
  - assist with beginners' course

Eric:
  - interested in beginners' course
  - formalize stable match algorithm 

Andrea:
  - implement higher inductive (inductive) types
  - printing: interactively reduce terms (discussion)

Ulf: Improve injectivity
  - constraint solver: pattern matching inversion ("injectivity")
  - currently does not work if one rhs is not rigid
  - improve: take specific use of "injective" function into account
      (since it might be partially applied already)

Stephan:
  - improve Agda GUI library
  - implement some basic functionality of an IDE
    (like Coq-IDE, Isabelle PIDE)
  - implement a fast sorting function in Agda

Andreas:
  - AutoZero: remake of the Auto
  - organize as a collection of micro-tactics


Jesper:
  - forced constructors (similar to Haskell lazy matches)
  - omega-in-omega: Inconsistent extension of universe polymorphism
  - discussion: gather the common imports in Agda .hs source files in our
      own "Prelude"
  - Q: how to handle pattern

      import Data.Map (Map)
      import qualified Data.Map as Map

  - postpone checking of definition by pattern matching
    new constraint: LHS problem
  - continue agda-spec project

Wrap up meetings

A short summary of the daily progress can be found here.

Excursion

The excursion will be on 1 February (Thursday). It will probably be a walk in the Buda hills followed by sitting in the hot water in a thermal bath. You should bring comfortable shoes (eg. hiking boots or running shoes) and swimming trunks.

Pictures

Location

The location is EIT Digital Co-Location Centre in Budapest, Hungary. Google Maps Link. There is a plastic red running path around the building. The entrance is from the back on the right hand side. There will be signs saying AIMXXVI. The building is five minutes walk from where the TYPES 2017 conference was.

Address:

    EIT Digital Budapest Node | Co-Location Centre
    10/a Bogdánfy Street
    H-1117 Budapest
    Hungary
    (corner of Warga László Str. and Bogdánfy Str.)
    GPS: N 47°28'28" E 19°3'27"

Photos of the building:

[] []

Currency

The currency is Hungarian Forint (HUF), around 300 HUF is worth 1 Euro. You can use debit/credit cards in almost every shop and restaurant, but you may need cash in small pubs. The cheapest way to get cash is from an exchange bureau in the city centre. Ask your hotel or follow these instructions.

Travel to Budapest

• By flight to Budapest Liszt Ferenc International Airport.
• By train: 2.5 hours journey from Vienna, direct trains from Berlin, Munich, Prague, Warsaw, Zurich etc. Search trains on bahn.de, buy tickets online from the respective train companies. International tickets from the Hungarian train company have to be printed at a kiosk at a train station in Hungary.
• By car: you can park your car next to the university for free at your own risk.

Travel from the airport to the city centre

• BKK bus 100E takes you to the city centre metro station Deák Ferenc tér. The bus starts just outside the terminal building. It starts on the hour and on the half-hour. You need a special ticket for it which costs 900 HUF (3 euros). You can buy this from the driver or from machines next to the bus stop at the airport. Google maps journey planner knows about the timetable.
• Airport minibus service, you can book it online or at the terminal in person after arrival.
• You can take a taxi from the airport, it is recommended to book a taxi at the Főtaxi kiosk just outside the terminal building.

Travel within the city centre

• Public transportation (BKK) is the fastest and cheapest way to get around in Budapest. You can use Google maps to plan your journey, it knows about all bus, trolley bus, tram and metro lines. It is recommended to buy a 5/30 BKK travelcard for 4550 HUF at the airport, you can use this for 5 times 24 hours during a month. Alternatively, you can buy 10 tickets for 3000 HUF: one ticket is only valid for a single bus/tram ride, if you change to another bus, you have to validate a new ticket (however you can change metro lines with a single ticket). You can buy tickets at the kiosk at the airport or from the ticket machines which accept debit/credit cards. There are machines next to the bus stop at the airport and at all metro stations, and at most tram stops. The conference venue is near the following BKK stops:
  • tram stop Petőfi híd budai hídfő
  • tram stop Infopark
  • bus stop Egyetemváros - A38 hajóállomás
  • boat stop Egyetemváros - A38 (the BKK boat stops on the Danube side of the A38 ship)
• Public bicycle: you can use the green public bicycles in the city centre, see BUBI website for information (BUBI = Budapest Bicycle). There is a BUBI docking station next to the conference venue. A weekly pass is 2000 HUF, and you can use a bicycle for 30 minutes without paying extra. You can buy a pass at the airport BKK kiosks or BKK Customer Service Points.
• Walking is cheap and nice.

Accommodation

Services such as booking.com and airbnb.com are known to work well in Budapest.

The judgemental map of Budapest is quite accurate about what the different areas are like. The conference venue is in the "more nerds" area.