Main /
\ Main

AIMXL

(redirected from Main.AIMXXXX)

The fortieth Agda Implementors' Meeting (AIM XL) will take place in Budapest, Hungary from 2025-05-26 to 2025-05-31 (Mon to Sat). 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.

Online participation

Teams meeting link

Program

Sunday, 25 May
18:30-Dinner in LUMEN, coming: Jesper, Szumi, Thorsten, Yee-Jian, Andrei, Iulia, Andreas, maybe Ambrus, Viktor, maybe Miëtek
Monday, 26 May
10:00Introduction Round, Talk Schedule
11:00Coffee break
11:30Ambrus Kaposi: Type Theory in Type Theory Using a Strictified Syntax
12:30Lunch
14:00Artem Shinkarov: Fixing very dependent types (discussion)
14:30Jesper Cockx: Rewrite rules tutorial
15:30Coffee break
16:00Andreas: Tutorial on Agda bugfixing
17:00Wrap up meeting

Dinner : 19:30, Alma & Koerte (Loerinc Pap Ter)

Tuesday, 27 May
10:00Thorsten Altenkirch: Higher Observational Type Theory in Narya
11:00Coffee break
11:30Ulf Norell: Thoughts on sound and complete validators
12:30Lunch
14:00Miëtek Bak: Lessons from a medium-scale formalization in Agda
15:00Coffee break
15:30Code sprints
17:00Wrap up meeting

Dinner : 18:30, Black Dog Pub

Wednesday, 28 May
10:00Yee-Jian Tan: Implementing computational UIP in Cubical Agda
11:00Coffee break
11:20We leave the big room and put our stuff in the meeting room to provide space for the Ottoman Empire
11:30Early lunch
14:00Code sprints
15:30Coffee break
16:00Code sprints
17:00Wrap up meeting
Thursday, 29 May
10:30We meet at tram stop Hűvösvölgy (end station of tram lines 56,56A,59B,61) -- you should bring water and maybe some snacks for the hike and swimming suit, towel, slippers for the thermal bath
14:00We arrive in restaurant Normafa síház, eat late lunch
16:30We go to Rudas thermal bath (open until 8pm; you should bring swimming stuff)
Friday, 30 May
10:00Péter Diviánszky: Efficient implementation of algebraic data types with rewrite rules
11:00Coffee break
11:30Balázs Kőműves: Write high-performance cryptography code in Agda
12:30Lunch
14:00Code sprints
15:30Coffee break
16:00Code sprints
17:00Wrap up meeting
Saturday, 31 May
10:00Code sprints
11:00Coffee break
11:30Szumi Xie: Secret bonus talk
12:30Lunch
14:00Code sprints
15:30Coffee break
16:00Code sprints
17:00Wrap up meeting

Registration

To register, you can fill out the following form and send it to akaposi <at> inf <dot> elte <dot> hu. Please advise us, if you don't want your name to be added to this webpage. You can also (if you are okay with your name being public) directly fill your name in the section participants on this webpage using the edit option for it. In this case, you can also directly add a talk / discussion / code sprint proposal by copy and pasting the box examples.

If you can not attend in person, it will be possible to attend online. You can register via email or directly by adding your name to the list.

to: akaposi <at> inf <dot> elte <dot> hu
Subject: Registration for AIM XL
  • Name:
  • Online or In person:
  • Add my name to the Meeting webpage (yes/no):
  • Affiliation:
  • If you wish to give a talk:
    • Title
    • Short Abstract (Optional)
  • If you wish to suggest a talk topic:
    • Topic
    • Short Description (Optional)
  • If you wish to suggest a code sprint:
    • Proposal
    • Short Description (Optional)
  • Other comments:

Participants

  • Ambrus Kaposi (ELTE)
  • Szumi Xie (ELTE)
  • Viktor Bense (ELTE)
  • Balázs Kőműves (Faulhorn Labs / Codex (IFT))
  • Péter DIviánszky (Faulhorn Labs)
  • Jesper Cockx (TU Delft)
  • Artjoms Šinkarovs (University of Southampton)
  • Yee-Jian Tan (IP Paris/KU Leuven)
  • Ulf Norell (Quviq)
  • Andreas Abel (Chalmers University of Technology and University of Gothenburg)
  • András Kovács (Chalmers University of Technology and University of Gothenburg)
  • Marcin Jan Turek-Grzybowski (from Wednesday)
  • Andrei Dorian Duma (University of Bucharest)
  • Iulia Dumitru (Politehnica University of Bucharest)
  • Thorsten Altenkirch (University of Nottingham)
  • Bohdan Liesnikov (TU Delft)
  • Arved Friedemann (independent, online)
  • Zhenyun Yin (ELTE)
  • Barabás Gergely Miklós (ELTE)
  • Miëtek Bak (Machine Intuitionist)
  • Amélia Liao (https://1lab.dev)
  • Peter Korpa (ELTE)
  • Áron Szabó (independent)
  • Kun Édua Boróka (ELTE)

Talk proposals

Please add your proposals here by editing this webpage (using the edit button). You can refer to examples from previous Agda Implementors meetings.

Efficient implementation of algebraic data types with rewrite rules
Péter Diviánszky
(no abstract yet)
Higher Observational Type Theory in Narya
Thorsten Altenkirch
Narya is an implementation of a Parametricity Type Theory which has been created by Mike Shulman and Elif Uskuplu. Using a higher coinductive type we can implement a variant of HoTT, which we call Higher Observational Type Theory. I would like to discuss how this relates to cubical agda and how Narya could benefit from an agda-like environment.
Some thoughts about sound and complete validators
Ulf Norell
A common task in dependently typed programming is taking some unverified input and checking that it satisfies some interesting property. Establishing soundness for such a validator we usually do by construction--the validator simply returns a value that intrinsically satisfies the property, but proving completeness is less obvious how to do nicely. I'll talk about what the various alternatives are and my experiences with them. Based on work very much in progress.
Implementing computational UIP in Cubical Agda
Yee-Jian Tan
By removing Glue types in Cubical Agda, then postulating the Uniqueness of Identity Proofs (UIP) assumption, we can have Quotient inductive types and provable functional extensionality, which are nice properties to have. I will talk about the current progress in 1. having a variant of Cubical Agda without Glue (and hence compatible with K and UIP), and on top of it, 2. a "Cubical - Glue + UIP" Agda with nice computational properties, such as UIP proofs over type formers being automatically generated by Agda.
Write high-performance cryptography code in Agda
Balázs Kőműves
We are trying to prove the concept of staged metaprogramming with two-level type theory, using Agda for prototyping. Practical cryptography requires a lot of metaprogramming, usually done with "macros", ad-hoc code generation, etc. We believe that even Agda should be better than those things! And (at least in theory) the resulting code can be pretty fast too.
Type Theory in Type Theory Using a Strictified Syntax
Ambrus Kaposi
I present a way to formalise replace any model of a theory with bindigs (precisely a first-order model of a second-order generalised algebraic theory, SOGAT) with an equivalent model where are substitution rules are definitional. This solves the transport hell issue when formalising e.g. the intrinsic syntax of type theory in Agda. Does this solution evoke another kind of hell?

Location

The location is EIT Digital Co-Location Centre of ELTE (Eötvös Loránd University) 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 AIMXL. 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"

The building is open 8am-4pm but we have one card to access the building outside of these times.

Lunch: Science Park

Currency

The currency is Hungarian Forint (HUF), around 400 HUF is worth 1 Euro. You can use debit/credit cards in almost every shop and restaurant, cash is rarely needed.

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.
  • By car: you have to pay for on-street parking near the venue, except at weekends. The easiest way to pay parking is a mobile app, e.g. Parkl.

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. You can pay using credit/debit card on the bus, no need to buy separate ticket (but possible from a purple machine next to the bus stop). It runs day and night, very regularly.
  • You can use minibus service or taxi, but I wouldn't.
  • You can cycle if you bring your bicycle on the plane: CyclOSM knows about the cycle paths.

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. You can buy a 2-week pass for 5950 HUF, or use individual tickets or use the BudapestGO app on your phone.
  • Public bicycle: you can use the green public bicycles in the city centre, see BUBI website for information (BUBI = Budapest Bicycle).
  • 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 venue is in the "more nerds" area.

Excursion

The excursion will be on *Thursday*. We will start with a hike in the Buda hills and a (late) lunch. After that we will go to a thermal bath. The hike will be an easy walk in the Buda hills, there is no need to take special equipment.

Jesper's pictures

Some random cultural programmes

  • free exam concerts at the music academy: see here
  • Budapest100 on the Saturday/Sunday of arrival
  • thermal baths, e.g. Rudas, Széchenyi

T-Shirts

€20 (preferred) or 8100 HUF (cash)

Pay Miëtek Bak

Sponsorship

AIM XL is supported by the HOTT ERC grant 101170308.

Code sprints

  • Agda LSP integration (Bohdan, Mietek, Andreas, Iulia)
  • Double checker for clauses (Bohdan, Amy)
  • Higher observational type theory (Ambrus, Thorsten, Artem, Szumi)
  • Non-quadratic operator parsing (Andras)
  • Fixing bugs in the Emacs mode (Mietek, Ulf, Iulia)
  • Cubical with UIP (Yee-Jian, Amy, Andras, Peter Korpa, Szumi)
  • Metaprogramming in Agda (Balázs)
  • Improving termination checking with cubical (Thorsten)
  • Dependent destructors for record types (Thorsten)
  • Postponing insertion of implicit arguments for blocked types (Mietek, Andras, Jesper)
  • Very dependent types (Artem)
  • Overloading of record projections (Amy)
  • `record where` syntax (Amy)
  • Rewrite rules on projections (Jesper)
  • Mimer: cleaning code, documentation, features (Ulf, Jesper, Amy, Mietek, Andreas)
  • Typst backend (Andreas)
  • Expanding search (C-c C-z) to include potential imports (Andrei, Peter Korpa)

Wrap-up notes

Rewrite rules

  • Monday: Jesper gave a talk and found a bug in the confluence checker [https://github.com/agda/agda/issues/7893]
  • Monday: Mietek experimented with rewrite rules in his formalization of first-order logic

Implicit arguments

  • Monday: Andras and Jesper discussed when insertion of implicit arguments and lambdas should/shouldn't happen
  • Tuesday: Experimented with a version of Agda that postpones type-checking terms when they might have an implicit function type (see https://github.com/agda/agda/tree/ImplicitLambdas). This fixes some test case and breaks everything else.
  • Tuesday: Worked on refactoring Unblock constraints and removing twin metas (this does NOT break everything)
  • Wednesday: Andras and Jesper experimented further with heuristics for when (not) to insert hidden lambdas
  • Wednesday: Jesper finished his PR https://github.com/agda/agda/pull/7899 but it fails on the cubical library.

Overloading of record projections

Expanding search

  • Monday: Andrei installed Agda and looked at the current code implementing C-c C-z
  • Tuesday: Andrei and Andreas investigated further, found that searching in all libraries is a lot more complicated than the current search in imports only. Need to construct an index for each library.

Experiments with metaprogramming

  • Tuesday: Balázs is implementing a demo application with metaprogramming
  • Wednesday: tiny progress, made two bug reports in the standard library

Mimer

  • Tuesday: Áron found a bug in Mimer, Ulf started to debug it
  • Wednesday: Ulf fixed the bug https://github.com/agda/agda/issues/7898. Mimer would put the solution in the Emacs buffer but didn't let Agda know about the solution.
  • Wednesday: Ulf started to break up the implementation of Mimer into different modules

Sound and complete type checkers in Agda

  • Tuesday: Ulf gave a talk, Peter started implementing it for STLC (or perhaps System F)
  • Tuesday: Andreas and Thorsten disagree on the meanings of soundness and completeness

Higher Observational Type Theory

  • Tuesday: Szumi tried to prove that the universe of contractible types is contractible, but ran into the same problem as with proving that the universe of fibrant types is fibrant
  • Wednesday: Ambrus wants an isomorphism, but there's only a section-retraction pair. At the moment there is some confusion but certainly progress.

Inlining of constructors

Double checking of case trees

  • Wednesday: Bohdan and Amy made a bit of progress

Cubical with UIP

  • Wednesday: Yee-Jian started to give a type signature for the new primitive
  • Wednesday: some discussions on the proper reduction behavior of definitional UIP

Positivity checking with transport

Edit | History | Recent Changes (all) | Search
Page last modified on May 29, 2025, at 07:34 pm
Powered by PmWiki