Agda Implementors' Meeting XLIII
- View
- Edit
- History
- 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.
- 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)
Main /
\\ Main
Agda Implementors' Meeting XLIII
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:
Location
Rzesz�w, Poland
The venue is at Przestrzeń konferencyjna, which is located close to the city center. Address: Teofila Lenartowicza 4 , 35-051 Rzesz�w.
Zulip stream
Please subscribe to the AIM XLIII channel on the Agda Zulip to get the latest updates and organize code sprints.
Food
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 | Talks / presentations (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: progress, blockers and plans |
Tuesday, 20 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: progress, blockers and plans |
Wednesday, 21 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 | 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. No ordinary talk or code-sprint sessions are scheduled for this day. The route, timings, meeting point, transport arrangements and any additional costs will be announced separately.
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 a soft registration deadline on tba. In order to ensure we have enough food and a room with sufficient capacity, please register soon!
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 | | 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 discussion topic: Topic Short Description (Optional) If you wish to suggest a code sprint: Proposal Short Description (Optional) If you work for a company: Are you willing to give a short (say 10 min) "industry talk" on why/how your company cares about Agda and/or related topics? It is interesting for the Agda community to know. Other comments (e.g. dietary restrictions for catering): |
Participants
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.
| Title | | -------------- | | Speaker | | Short abstract |
| Type-based Library Search for Agda | | ----------------------------------------------------------- | | Speaker: Satoshi Takimoto (Institute of Science Tokyo). |
---
Excursion
---
AI Demos and Discussions session
---
Discussions
| Code sprint | | --------------- | | Participants | | Short abstract |
| Discussion: Type-based proof search | | --------------------------------------------------------------------------------- | | Proposed by: Silas Hayes-Williams (University of Nottingham). | | Reference: Agda pull request #8664. |
Code sprints + wrap-up notes
Acknowledgements
Edit | History | Recent Changes (all) | Search
Page last modified on September 30, 2026, at 07:09 am
Powered by PmWiki