The forty-third Agda Implementors' Meeting (AIM XLIII) will take place in Rzesz�w, Poland from 2026-10-19 to 2026-10-24 (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.
- Opportunities to write your first Agda programs and proofs and meet its developers and users.
- Plenty of time to work on or in Agda, in collaboration with the other participants.
Watching talks online
links to talks, will be posted on AGDA zulip, in #AIM XLIII channel
Help and contact
Organisers' phone: +48 538 151 590
Need assistance or have a question? Please feel free to call us at any time during the meeting � including late at night or early in the morning. We're happy to help!
Location
Rzesz�w, Poland
The venue is at Przestrzeń konferencyjna, which is located close to the city center. Address: Teofila Lenartowicza 6 , 35-051 Rzesz�w, second floor.
Zulip stream
Please subscribe to the AIM XLIII channel on the Agda Zulip to get the latest updates and organize code sprints.
Food
Dinner on Wednesday, 21 October
During the Agda Implementors' Meeting, we plan to have a dinner on Wednesday, 21 October at the Polish restaurant Folk (see the menu). Since we need to have a final head count for the reservation, we kindly ask you to send a short message indicating if you are coming to the dinner (yes/no) to xliii.agda.implementors.meeting@gmail.com. Please do so as soon as possible. The prices in the restaurant are around 20�30 euro.
While menu does not list vegan option, we were ensured by the venue that vegan main course will be available if we will give them prior notice.
Program
Provisional schedule. The daily timings below are proposed and may change. All times are local to Rzesz�w (Europe/Warsaw).
Individual talks and presentations have not yet been assigned to time slots. They are listed separately under Talk proposals, with discussion topics under Discussions. The detailed allocation of talks and code sprints will be agreed with participants at the opening session.
Afternoons are primarily reserved for collaborative work on and with Agda. Unused talk slots will be available for code sprints and discussions. Breaks reserve time in the programme; catering arrangements will be announced separately.
Monday, 19 October
| Time | Activity |
|---|---|
| 09:30-10:30 | Welcome, introductions, code-sprint proposals and programme planning |
| 10:30-11:00 | Morning break |
| 11:00-12:30 | "Smart with" demo - Nathaniel Burke (TU Delft) |
| 12:30-14:00 | Lunch break |
| 14:00-15:30 | Code sprints |
| 15:30-16:00 | Afternoon break |
| 16:00-17:30 | Code sprints and small-group discussions |
| 17:30-18:00 | Daily wrap-up: progress, blockers and plans |
Tuesday, 20 October
| Time | Activity |
|---|---|
| 09:30-10:30 | Type-based Library Search for Theorem Provers - Satoshi Takimoto (Institute of Science Tokyo) |
| 10:30-11:00 | Morning break |
| 11:00-12:30 | Logical Frameworks and Language Workbenches for Dependent Type Systems - Jesper Cockx |
| 12:30-14:00 | Lunch break |
| 14:00-15:30 | Code sprints |
| 15:30-16:00 | Afternoon break |
| 16:00-17:30 | Code sprints and small-group discussions |
| 17:30-18:00 | Daily wrap-up: progress, blockers and plans |
Wednesday, 21 October
| Time | Activity |
|---|---|
| 09:30-10:30 | How to Compute with HIIT Reals - Lorenzo Molena |
| 10:30-11:00 | Morning break |
| 11:00-12:30 | Code sprints and follow-up discussions |
| 12:30-14:00 | Lunch break |
| 14:00-15:30 | AI demos and presentations |
| 15:30-16:00 | Afternoon break |
| 16:00-17:30 | Code sprints and follow-up discussions |
| 17:30-18:00 | Daily wrap-up: progress, blockers and plans |
Thursday, 22 October
| Time | Activity |
|---|---|
| 09:30-10:30 | Talks / presentations (to be scheduled) |
| 10:30-11:00 | Morning break |
| 11:00-12:30 | Talks / discussions (to be scheduled) |
| 12:30-14:00 | Lunch break |
| 14:00-15:30 | Code sprints |
| 15:30-16:00 | Afternoon break |
| 16:00-17:30 | Code sprints and small-group discussions |
| 17:30-18:00 | Daily wrap-up and practical information for Friday |
Friday, 23 October
Excursion.
Friday is reserved for the excursion to Wieliczka Salt Mine. No ordinary talk or code-sprint sessions are scheduled for this day. The details are bellow.
Saturday, 24 October
| Time | Activity |
|---|---|
| 09:30-10:30 | Code sprints |
| 10:30-11:00 | Morning break |
| 11:00-12:30 | Code sprints and informal demonstrations |
| 12:30-14:00 | Lunch break |
| 14:00-15:30 | Code sprints, documentation and follow-up planning |
| 15:30-16:00 | Afternoon break |
| 16:00-16:30 | Final wrap-up: results, remaining work and next steps |
The proposed finish on Saturday is 16:30; the final closing time and room-access arrangements are still to be confirmed.
Registration
Registering for the meeting is free but mandatory. There is NO registration deadline! Please register as soon as posible in order to ensure we have enough food and a room with sufficient capacity.
To register, you can fill out the following form and send it to xliii.agda.implementors.meeting@gmail.com . 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 there is demand for it, it might be possible to attend online. Please contact the organizers directly so we can make the necessary preparations.
| to: |
| Subject: Registration for AIM XLIII |
|
Participants
- Marcin Grzybowski (organizer)
- Jesper Cockx (TU Delft)
- Andreas Abel (Chalmers/Gothenburg University)
- Yee-Jian Tan (KU Leuven)
- Andr�s Kov�cs (University of Cambridge)
- Nathaniel Burke (TU Delft)
- Andre Knispel? (IOG)
- Satoshi Takimoto (Institute of Science Tokyo)
- Lorenzo Molena (University of Verona)
- Hans-J�rg Schurr (Inria, LMF, France)
- Silas Hayes-Williams (she/they) (University of Nottingham)
- Krystian Nieradko (FormalFoundry.ai)
- Jackson Brough (University of Utah)
- Ana Pantilie (Midgard Labs)
- Jan Pieprzycki (FormalFoundry.ai)
- Mi�tek Bak (Adam Mickiewicz University)
- Piotr Paradziński
- Fabian Alonso (online)
- Grzegorz Kunicki (FormalFoundry.ai)
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.
| Type-based Library Search for Theorem Provers |
| Satoshi Takimoto (Institute of Science Tokyo) |
| In this talk, I present ongoing research with Jesper Cockx on type-based library search for theorem provers. I first give a brief background and establish the problem setting and research direction. Next, we start with a simpler setting, System F, and investigate the feasibility of the approach there. Finally, I discuss the challenges that arise when extending the approach to dependent type theory. This research is very much work-in-progress, and the presentation will be open-ended. |
| Programming and Proving in Agda |
| Jesper Cockx |
| For anyone who is new to dependently typed programming and/or Agda, I would be happy to give an introduction to the language and some of the underlying theory. |
| Logical Frameworks and Language Workbenches for Dependent Type Systems |
| Jesper Cockx |
| Since its inception, Agda has served as a playground for experimenting with new type systems and language features. However, adding more and more features to Agda is not scalable and creates a high burden of maintenance. Nevertheless, implementing a new dependently typed language from scratch is a daunting task so the desire to keep extending Agda further still remains. Are there any alternatives? In this talk, I will compare two different approaches towards the goal of easily and declaratively specifying new dependently typed languages: logical frameworks such as Twelf and Dedukti and language workbenches such as Spoofax and Rascal. I particularly want to highlight work by several of my students aimed at combining the benefits offered by each approach and point at possible directions for future work in this area. |
| Smart with |
| Nathaniel Burke |
| I have been working on an improved version of Agda's "with"-abstraction construct (and I am planning to spend time polishing it during the meeting). I want to give a short demo, and hopefully convince some people to try it out/report bugs! The implementation currently lives here. |
| Title |
| Speaker |
| Short abstract |
Excursion � Friday, 23 October
We will visit the Wieliczka Salt Mine, with its underground chambers, salt sculptures and St Kinga's Chapel. We plan to take the Tourist Route with an English-speaking guide. It will also be a chance to get to know one another away from the talks and code sprints.
We will travel by train from Rzesz�w, leaving no earlier than 10:00. On the way back, weather permitting, we will spend about two hours in Krak�w for a short walk around the Old Town and time for food or coffee before returning to Rzesz�w in the evening.
Proposed plan
The times below are approximate planning targets, not confirmed train departures or a booked tour slot. Exact trains, the mine entry time and the assembly details will be confirmed here before the excursion. All times are local to Poland.
| Approximate time | Activity |
|---|---|
| 10:00-10:30 | Departure from Rzesz�w Gł�wny by train. We will meet at the station before departure; the precise meeting point and time will be announced. |
| Late morning / early afternoon | Change at Krak�w Gł�wny for the regional train to Wieliczka Rynek-Kopalnia. Walk to the mine, with time for a light lunch and to assemble before the tour. |
| 13:30-16:30 | Target window for the guided mine visit. |
| 16:30-17:30 | Return to the surface, walk to the station and travel back to Krak�w Gł�wny. |
| 17:30-19:30 | Optional two-hour stop in Krak�w if the weather is suitable, including the walk back to the station. |
| Around 20:00 | Return train from Krak�w to Rzesz�w; exact service to be confirmed. |
| Around 21:30-22:00 | Target arrival back in Rzesz�w, depending on the final train arrangements. |
Travel and meeting points
The planned route is Rzesz�w Gł�wny � Krak�w Gł�wny � Wieliczka Rynek-Kopalnia, returning via Krak�w. The Krak�w�Wieliczka leg uses the SKA1 regional train and takes approximately 25 minutes.
The Tourist Route starts at the Daniłowicz Shaft, Daniłowicza 10, Wieliczka, a short walk from Wieliczka Rynek-Kopalnia station. See the mine's map and access information.
Please coordinate with the organisers before buying separate tickets, particularly if you would like to join us in Krak�w or Wieliczka, or stay in Krak�w afterwards.
Krak�w stop and weather
If the weather is pleasant, we plan a relaxed Old Town walk and some free time for food or coffee. The two-hour stop includes getting back to Krak�w Gł�wny; please be at the agreed meeting point at least 20 minutes before our onward train.
The mine visit itself is underground and is planned to go ahead in ordinary rainy weather. If the weather is poor, we will skip the sightseeing walk. We will confirm the return plan before departure; an earlier return will depend on the trains and ticket arrangements, otherwise the waiting time can be spent indoors.
What to bring and accessibility
- Comfortable walking shoes and an extra layer. The Tourist Route involves approximately 3.5 km of walking and around 800 steps, including a long initial descent. The return to the surface is by lift. The underground temperature is around 17-18 degrees Celsius.
- Water and something to eat for the journey. Please plan to eat before the underground tour rather than wait until the Krak�w stop. Bring suitable clothing for the outdoor parts of the day, including possible rain.
- Only a small bag. The mine permits hand luggage no larger than 35 x 20 x 20 cm. Please leave larger bags at your accommodation; luggage-locker availability at the mine is limited.
- Please tell us in advance about accessibility needs. The standard route includes many stairs. Adapted visits are available for parts of the mine by prior arrangement, but should not be assumed to follow our group's route or timetable.
See the mine's practical visitor information.
Participation, cost and contact
All travel tickets and admissions cost wont exceed 220zl (~50 euro)
AI and Agda: informal demos and experience reports
Wednesday, 21 October 14:00
An informal session for sharing experiments with LLMs, AI tools and agents, both for developing Agda itself and for writing programs, proofs and libraries in Agda.
Contributions can take anywhere from 2 to 30 minutes. You might share your experience using Claude or Codex without any special setup, demonstrate a customised workflow or agent, or show experiments on a modified Agda branch. A small example, an unexpected result or a question arising from your own work is enough � you do not need to have built a new tool.
Failures and limitations are just as welcome as successes. Show something that worked, something that went wrong, or something that took more effort than doing it yourself. Optimistic, sceptical and critical perspectives on AI in Agda and other proof assistants are equally welcome: this is a chance to compare actual experiences, not a showcase restricted to positive results.
No polished presentation or slides are required. Bring a live demo, a recorded interaction, some code, or simply an experience to discuss. You are also welcome to join just to watch, ask questions and contribute to the conversation.
There will be oportunity to join remotely!
Discussions
| 20 years of Agda: what have we learned? |
| Jesper, ? |
| After developing Agda for over 20 years, a lot of design decisions that were made early in the development have shown themselves to be suboptimal. Some examples include the lack of internal representation for let-bound variables, lambda-lifting of local definitions, the desugaring of module parameter applications, the lack of sharing during conversion checking and elaboration, and probably many more. Even if we cannot revert these decisions easily, it would be good to document them somewhere for longer-term planning or an eventual re-implementation of Agda. |
|
Discussion: Type-based proof search |
|
Proposed by: Silas Hayes-Williams (University of Nottingham). |
|
Reference: Agda pull request #8664. |
Code sprints + wrap-up notes
| Code sprint: Quality of life improvements to opaque |
| Participants: Jesper, Marcin, Lorenzo |
| Short abstract: See #8757 |
| Code sprint: Fix subject reduction issue with Setω |
| Participants |
| Short abstract: See #5810. We came up with a plan for this last AIM but didn't finish implementing. |
| Monday: Jesper thought about this, but no concrete progress. |
| Code sprint: Incremental case tree construction |
| Participants: Jesper, Andreas |
| Short abstract: The end goal here is to remove clause-based matching (which was the cause of several recently-found soundness bugs). |
| Code sprint: User-definable eta rules |
| Participants: Nathaniel (maybe, I have other code sprints to finish first) |
| Short abstract: It would be nice to have a rewrite rule-like mechanism for (type-directed) eta rules. We could use it to get eta for inductive families #4319 and implement rules like `univ-ext` from Sterbac and Sterling's "Fuss Free Cumulative Universes" |
| Cubical real analysis |
| Lorenzo,Jackson,Marcin |
| Short abstract |
| Monday: Lorenzo has been working on a code snippet for improving efficiency of computing with reals. |
| Cubical with UIP |
| Participants: Yee-Jian |
| Short abstract |
| Monday: Yee-Jian rebased his branch to Agda 2.9.0 |
| Type-based library search tool |
| Satoshi |
| Short abstract: polish my prototype tool https://github.com/wasabi315/aegle |
| Monday: Satoshi prepared his presentation for tomorrow. |
| Smart with |
| Participants: Nathaniel |
| Implemented here. I need to polish and fix bugs. If anyone wants to test it, that would be highly appreciated! |
| Monday: Nathaniel gave presentation and did some rebasing, now working on improving error messages |
| Agda2Scala |
| Participants: Piotr |
| Short abstract: Make an Agda backend to generate Scala 2/3 code. Concrete goal: handling of higher-kinded types (i.e. parametrized/indexed types in Agda). |
| Agda MCP |
| Participants: Jackson, Marcin, Mietek |
| Short abstract: Concrete goal is to finish the current MCP implementation and command-line interface (https://github.com/broughjt/agda-mcp) and perhaps integrate it into the main Agda repo. |
| Bytestring library and bit operations |
| Participants: Ana, Marcin, Jan |
| Short abstract: Goal is to publish this as a standalone library |
| Code sprint |
| Participants |
| Short abstract |