Agda Implementors' Meeting XLI

The forty-first Agda Implementors' Meeting (AIM XLI) will take place in Angers, France from 2025-11-24 to 2025-11-29 (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.

Program

Registration

Registering for the meeting is free but mandatory. There is a soft registration deadline on 24 October. Registrations might be closed after this date due to the limited capacity of the room (30 people), so register soon!

To register, you can fill out the following form and send it to j.g.h.cockx@tudelft.nl. 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.

Participants

• Nicolas Pouillard, local organizer
• Jesper Cockx (TU Delft), co-organizer
• Vojta Štěpančík (INRIA)
• Yee-Jian Tan (KU Leuven)
• Henry Blanchette (University of Maryland)

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.

Location

The location is La Bulle en Bois and is a so-called Third Place. Namely, a hybrid combination of work and non-work activities. The place includes:

• A coworking place with shared offices and meeting rooms.
• A canteen with locally cooked food (vegan & organic)
• A fablab (3d printing, laser cutting)

Address: 11 rue Alexandre Fleming 49000 ANGERS

Lunch: Lunch is available on site on week days, cooking here is vegan and we have alternatives.

Travel to Angers

Best recommendations to travel to Angers : How do I get to Angers?.

Getting around in Angers

Irigo is the name of the transportation network in Angers. Maps and itineraries are on there website : Irigo.fr.

By Tram

La Bulle en Bois is located next to the university campus, hence easily reachable by Tram. The stop is called Belle-Beille Campus, this is the terminus of line C.

For instance there is a direct connection from the main train station Gare Angers Saint-Laud and it is a 22min ride.

By Bike

The city is bike friendly, you can rent one either for your whole stay of for each ride : Rent a bike in Angers.

From the main train station to La Bulle en Bois, this is 18min ride.

Accommodation

tba

Note from Jesper: I have made a preliminary booking (still cancellable) for an apartment in downtown Angers with 4 bedrooms / 6 beds, please contact me if you are interested to share.

Excursion

tba

Sponsorship

The location for the meeting is provided free of charge very kindly by La Bulle en Bois.

Code sprints

• Using Agda macros as interactive tactics (Henry Blanchette)

Short Description: It should be possible to use Agda's macro capabilities to emulate the features of interactive tactics LTac in Coq/Rocq. Agda's typed holes already get almost all the way there; they just need to handle interactive holes well!

• ...

Wrap-up notes

Code sprint 1

• Monday: ...
• Tuesday: ...

Code sprint 2

• Monday: ...
• Tuesday: ...