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
| Sunday, 23 November | |
|---|---|
| 18:30- | Dinner (tba) |
| Monday, 24 November | |
| 9:30 | Introduction Round, Talk Schedule |
| 10:30 | Coffee break |
| 11:00 | Talk 1 |
| 12:30 | Lunch |
| 14:00 | Code sprints / discussions |
| 15:30 | Coffee break |
| 16:00 | Code sprints / discussions |
| 17:30 | Wrap up meeting |
| Tuesday, 25 November | |
| 9:30 | Talk 2 |
| 10:30 | Coffee break |
| 11:00 | Talk 3 |
| 12:30 | Lunch |
| 14:00 | Code sprints / discussions |
| 15:30 | Coffee break |
| 16:00 | Code sprints / discussions |
| 17:30 | Wrap up meeting |
| Wednesday, 26 November | |
| 9:30 | Talk 4 |
| 10:30 | Coffee break |
| 11:00 | Code sprints / discussions |
| 12:00 | Lunch |
| 13:00 | Excursion (tbd) |
| Thursday, 27 November | |
| 9:30 | Talk 5 |
| 10:30 | Coffee break |
| 11:00 | Talk 6 |
| 12:30 | Lunch |
| 14:00 | Code sprints / discussions |
| 15:30 | Coffee break |
| 16:00 | Code sprints / discussions |
| 17:30 | Wrap up meeting |
| Friday, 28 November | |
| 9:30 | Talk 7 |
| 10:30 | Coffee break |
| 11:00 | Talk 8 |
| 12:30 | Lunch |
| 14:00 | Code sprints / discussions |
| 15:30 | Coffee break |
| 16:00 | Code sprints / discussions |
| 17:30 | Wrap up meeting |
| Saturday, 29 November | |
| 10:00 | Code sprints / discussions |
| 10:30 | Coffee break |
| 11:00 | Talk 9 |
| 12:30 | Lunch |
| 14:00 | Code sprints / discussions |
| 15:30 | Coffee break |
| 16:00 | Final wrap up meeting |
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.
| to: j.g.h.cockx@tudelft.nl |
| Subject: Registration for AIM XLI |
|
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)
- Ana Pantilie (IOG)
- Jacco Krijnen (IOG)
- Peter Mosses (TU Delft)
- Nathaniel Burke (TU Delft)
- Andrei Duma (Dumco Digital)
- Iulia Dumitru
- Andreas Abel (Chalmers & U Gothenburg)
- András Kovács (Chalmers & U Gothenburg)
- Naim Favier (Chalmers & U Gothenburg)
- Amélia Liao
- Áron Szabó
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.
| Certified Compilation of Untyped Plutus Core |
| Ana Pantilie |
| Untyped Plutus Core (UPLC) is the language evaluated on the Cardano blockchain, therefore it is the compilation target for all Cardano smart contract languages, such as Plinth. Based on Jacco Krijnen's work on Translation certification for smart contracts, we have implemented (in Agda and Haskell) a proof-of-concept certifier for the UPLC optimisation phase of the Plinth compiler. This component produces compilation certificates in the form of Agda proofs. |
| Postulating Domains for Lightweight Formalization of Denotational Semantics |
| Peter Mosses |
| For lightweight formalization of denotational semantics, we treat ordinary Agda types as domains, and postulate required properties (such as the existence of least elements, and of a function that returns fixed points of arbitrary endofunctions). Current examples using such a formalization include the untyped λ-calculus, PCF, and a simple sublanguage of Scheme. It appears that the unsoundness of the postulates does not affect the Agda type-checker. In the talk, after illustrating the simplicity of lightweight formalization, we consider the possibility of replacing the current postulates by sound postulates for synthetic domain theory in Agda. |
| What's new in Agda2Hs |
| Jesper Cockx |
| Agda2Hs is an Agda backend for producing verified and readable Haskell code from a restricted subset of Agda. It makes extensive use of erasure annotations (aka the 0 quantity from QTT) to decide which parts of a program should be erased during the translation to Haskell. In this talk I would like to highlight a few of the different options that Agda2Hs provides to further tweak the generated Haskell code. In particular: unboxed records (records that compile to the value of their unique non-erased field), tuple records (records that are compiled to a Haskell tuple), inline functions (functions that can be reduced away before translation), and compile-to pragmas (compiling multiple data types or functions to the same Haskell definition). I also want to take this opportunity to call for help with some of the currently open issues in Agda2Hs. |
| Talk title |
| Speaker |
| (no abstract yet) |
| Numerical instability or something more fundamental? |
| Áron Szabó |
| (no abstract yet) |
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
Excursion
tba
Sponsorship
The location for the meeting is provided free of charge very kindly by La Bulle en Bois.
Discussions and code sprints
| Using Agda macros as interactive tactics |
| Henry Blanchette |
| 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! |
| Adding sort & erasure information to treeless syntax |
| Jesper Cockx |
| See issues #753, #4193, #4733, and #5315 |
| Implement local rewrite rules |
| Jesper Cockx |
| See https://github.com/TheoWinterhalter/local-comp |
| Generating websites from literate Agda |
| Peter Mosses |
| The Makefile in https://github.com/pdmosses/xds-agda generated the website at https://pdmosses.github.io/xds-agda/ from plain and literate Agda files. Would it be of interest to generate such a website from the README modules in the Agda standard library? See https://pdmosses.github.io/agda-stdlib/ for an initial proposal. |
| Code sprint title |
| Participants |
| short description |
- ...
Wrap-up notes
Code sprint 1
- Monday: ...
- Tuesday: ...
Code sprint 2
- Monday: ...
- Tuesday: ...