The forty-third Agda Implementors' Meeting (AIM XLIII) took place in Rzeszów, Poland from 2026-10-19 to 2026-10-24 (Mon to Sat). The meeting was 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:00 | Code sprints and follow-up discussions |
| 15:00-16:30 | AI demos and presentations |
| 16:30-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. |
| agda2scala - experimental Agda backed for Scala2 and Scala3 |
| Piotr Paradziński |
| https://github.com/lemastero/agda2scala |
| 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 |
- Generate opaque definitions also from reflection, steer unfolding definitions from reflection (see #8861)
- Locally make decision about which definitions should be unfolded: pragma that turns off some reductions locally (would not endanger subject reduction) (see | #8860
| Thursday: Marcin continued working on a prototype |
| 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. |
| Tuesday, Wednesday: free variable check not closed under substitution; add extra argument to piSort which is a postponed occurrence check; Nathaniel: WIP: reduce piSort already during instantiate |
| Thursday: Nathaniel continued working on this. The basic issue is now fixed but there are a couple of other regressions. Currently debugging those. |
| Saturday: PR is ready (#8870), comments from Andreas are addressed. |
| 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: Option/pragma to disable injectivity/conflict/cycle unification rules |
| Participants: Nathaniel |
| Short abstract: Tom de Jong was requesting this for "foundation/pedagogical reasons". If we added a pragma to disable these rules per-datatype, we could also use it to make Licata's trick sound (https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/#comment-80163). |
| 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" |
| agda2hs |
| Jesper, Hans, Satoshi |
| import system https://github.com/agda/agda2hs/issues?q=is%3Aissue+state%3Aopen+import |
| Monday: We discussed plans. First step: always generate export lists. |
| Tuesday, Wednesday: always generate export lists for modules in agda2hs. Hit an obstacle: haskell-src-exts does not support operators in data export lists. |
| Thursday: Satoshi: added module export lists to agda2hs, PR got merged (https://github.com/agda/agda2hs/pull/466). Next step: re-exports. |
| Thursday: Jesper worked on updating Agda2Hs to Agda 2.9 |
| Saturday: Satoshi is working on translating module re-exports. Information is tricky to get from the ScopeInfo, so currently exploring a solution that re-parses and re-scopechecks the source. |
| Cubical real analysis |
| Lorenzo, Jackson, Marcin |
| Short abstract |
| Monday: Lorenzo has been working on a code snippet for improving efficiency of computing with reals. |
| Wednesday: Improve a bound in an example (demo). |
| Thursday: Lorenzo is working on real numbers library, refactoring Lipschitz definition |
| Saturday: Lorenzo added code to convert between Cauchy sequences indexed by natural numbers and by rational, and adding more control over how fast sequences converge. |
| Cubical with UIP |
| Participants: Yee-Jian |
| Short abstract |
| Monday: Yee-Jian rebased his branch to Agda 2.9.0 |
| Thursday: Yee-Jian gave a demo of sqFill primitive for cubical UIP, now works for record types |
| Type-based library search tool |
| Satoshi |
| Short abstract: polish my prototype tool https://github.com/wasabi315/aegle |
| Monday: Satoshi prepared his presentation for tomorrow. |
| Tuesday: Presentation. |
| Wednesday: Piotr fixed an issue with names. |
| Saturday: Satoshi merged a PR by Piotr that fixes a bug |
| 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 |
| Tuesday: documentation page written |
| Saturday: Nathaniel is re-enabling display forms and refactoring some of the code to remove duplication between smart and dumb with. |
| 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). |
| Wednesday: Functor example partially works; path-dependent types work; theorems about equality converted to property tests (early stage) |
| Saturday: Functor instances now fully functional. |
| 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. |
| Saturday: Jackson gave a demo and we had a discussion about it. Jackson did some refactoring. |
| Bytestring library and bit operations |
| Participants: Ana, Marcin, Jan |
| Short abstract: Goal is to publish this as a standalone library |
| Reload performance in parallel mode |
| Participants: Andras Kovacs |
| Short abstract: parallel mode parses files while sequential mode only looks at hashes |
| Wednesday: implementation almost finished, not yet tested |
| Thursday: Andras gave a demo of optimization for reloading previously loaded Agda files with -j (PR incoming) |
| Saturday: Andras gave another demo, performance improvement for reloading is now more dramatic. |
| Integrating SMT solvers with Agda |
| Participants: Marcin |
| Short abstract: Automatically produce postulates based on the semantics of SMT queries. Eventually, extracting proofs would be even better. |
| Saturday: Marcin worked on a prototype of a simple new integration and gave a demo, will land on Github later today |