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.
- Registration deadline (not strict).
- 2018-01-29 (Mon) to 2018-02-03 (Sat)
- AIM XXVI
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:
- 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
|09.30||Session 1: Talks & Discussions|
|11.00||Session 2: Talks & Discussions|
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
|Sunday, 28 January|
|19.30||Dinner, Szatyor bár (1111 Budapest, Bartók Béla út 36.) Food served until 22.30.|
|Monday, 29 January|
|15.00||Jesper Cockx: Elaborating left-hand sides of definitions by pattern matching|
|Tuesday, 30 January|
|09.30||András Kovács: Sharing-Preserving Elaboration with Precisely Scoped Metavariables slides|
|13.15||Stephan Adelsberger: On implementing GUIs in Agda|
|Wednesday, 31 January|
|16.00||Fredrik Nordvall Forsberg: Quotient Inductive-Inductive Types|
|17.30||Ambrus Kaposi: Higher Inductive-Inductive Types slides|
|Thursday, 1 February|
|9.00||Meeting at the statue at Móricz Zsigmond körtér.|
|cca 9.10||Take tram 56A or 61 to Hűvösvölgy (last stop)|
|cca 9.50||Walk from Hűvösvölgy to János-hegy (4.3 km, 321 m elevation)|
|cca 11.50||Walk from János-hegy to Normafa (2.3 km, 34 m elevation)|
|cca 12.20||Lunch in Normakert|
|cca 14.00||Walk from Normafa to bus stop "Tamási Áron utca / Thomán István utca" (3.9 km, 199 m descent)|
|cca 15.00||Take bus 110 or 112 towards "Bosnyák tér", get off at "Döbrentei tér"|
|cca 15.30||Go to Rudas thermal bath. Entrance fee: 3500 HUF.|
|Friday, 2 February|
|11.00||Guillaume Allais: A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs (github)|
|Saturday, 3 February|
|16.30||Péter Diviánszky: Type inference calculus (an alternative presentation of Andras' scoped metavariables)|
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.
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.
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.
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:
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:
- 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.
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.