Main /
\ Main

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.

Zulip stream

Please subscribe to the AIM XLI stream on the Agda Zulip to get the latest updates and organize code sprints.

Program

Note: the schedule for the talks is still preliminary and will be made final at the start of the meeting.

Sunday, 23 November
18:30-Dinner at La Cour. Please register via this form!
Monday, 24 November
9:30Introduction Round, Finalizing Talk Schedule
10:30Coffee break
11:00Matthieu Sozeau: Bounded cumulative universe polymorphism with algebraic universes: design, mechanized metatheory and implementation slides
12:30Lunch
14:00Yee-Jian Tan: Setoid Heaven?
15:00Code sprints
15:30Coffee break
16:00Code sprints / discussions
17:30Wrap up meeting
Tuesday, 25 November
9:30Jacco Krijnen, Ana Pantilie: Certified Compilation of Untyped Plutus Core
10:30Coffee break
11:00Peter Mosses: Postulating Domains for Lightweight Formalization of Denotational Semantics
12:30Lunch
14:00Andreas: Sustaining the Agda development
15:00Code sprints
15:30Coffee break
16:00Code sprints / discussions
17:30Wrap up meeting
19:00Dinner at Numero 10 (https://maps.app.goo.gl/G7SMDuf6U3iy6q1F6)
Wednesday, 26 November
8:15Hiking from the city center to the venue (meet at Pont des Arts et Metiers https://maps.app.goo.gl/kuDMZeBwBbNVKzTP7)
9:30Andre Knispel: Adventures in dependently typed programming - categorical cryptography edition
10:30Coffee break
11:00Lucas Escot: agda2lambox
12:00Go to city center for lunch
12:30Lunch in the city center. Suggested places: Potiron & Ciboulette (https://maps.app.goo.gl/ecVEwQrG3CC9KnmS8) or Maison Watson (https://maps.app.goo.gl/Ng3xAZz6cGJKqp9a8). Both are quite small, so it's best to split up.
14:30Excursion: meeting at Angers castle (https://maps.app.goo.gl/TgCPq29yN5ptTFqU7)
Thursday, 27 November
9:30Thomas Lamiaux: Working Nested Inductive Typed for Rocq and Lean
10:30Coffee break
11:00Áron Szabó: Numerical instability or something deeper?
12:30Lunch
14:00Discussion on HTML generation
15:00Code sprints
15:30Coffee break
16:00Code sprints / discussions
17:30Wrap up meeting
Friday, 28 November
9:30Jaro Reinders: Correct by Construction Design and its Challenges in Agda
10:30Coffee break
11:00Jesper Cockx: What's new in Agda2Hs
12:30Lunch
14:00Code sprints / discussions
15:30Coffee break
16:00Code sprints / discussions
17:30Wrap up meeting
Saturday, 29 November
10:00Code sprints / discussions
10:30Coffee break
11:00Nicolas Pouillard: Leeloo demo
12:30Lunch
14:00Code sprints / discussions
15:30Coffee break
16:00Final 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
  • 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)
  • Other comments:

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
  • Andreas Abel (Chalmers & U Gothenburg)
  • András Kovács (Chalmers & U Gothenburg)
  • Áron Szabó
  • Thomas Lamiaux (Wednesday - Friday)
  • Lucas Escot (IOG)
  • Sylvain HENRY (IOG)
  • Carlos Tomé Cortińas (IOG)
  • Jaro Reinders (TU Delft)
  • Marcin Jan Turek-Grzybowski
  • Lorenzo Molena
  • Andre Knispel (IOG)
  • Thiago Felicissimo (Inria) (Monday - Wednesday)
  • Matthieu Sozeau (Inria) (Monday)
  • Yannick Forster (Inria) (Monday)

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.

Bounded cumulative universe polymorphism with algebraic universes: design, mechanized metatheory and implementation
Matthieu Sozeau (@mattam82)
Building on a mechanically verified (in MetaRocq) refinement of the novel loop-checking algorithm of Bezem and Coquand, we present a new design and implementation of cumulative universe polymorphism for dependent type theories, materialized in a branch of the Rocq prover. Our system handles universe level polymorphism for the full algebra (l,0,+1,max), using (weakly) polynomial time constraint satisfiability and validity checking algorithms. We also generalize the notion of variance of universes to cumulative definitions, and design a principled simplification algorithm allowing to infer sensible abstractions of universes and constraints for implicitly universe polymorphic definitions and proofs. The system also supports mixed explicit and implicit universe inference and checking. We will present all these aspects along with examples and our preliminary performance benchmarks and compatibility status. Extension of this system to larger hierarchies (e.g. with \omega + n) and first-class universe quantifications as present in Agda is an open question.
Certified Compilation of Untyped Plutus Core
Jacco Krijnen, 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.
Working Nested Inductive Typed for Rocq and Lean (Nantes's team)
Thomas Lamiaux
Nested inductive types, such as RoseTree, are fundamental in formalizing computer science, as they can model complex syntax like pattern-matching constructors. Consequently, they are widely used in major projects such as CompCert, Iris, and MetaRocq. Yet, neither Rocq nor Lean currently provides adequate support for them. Rocq and Lean accepts different class of inductive types. Rocq accepts an overly permissive class of nested inductive types, including some that actually correspond to inductive-inductive types. In contrast, Lean is overly restrictive, rejecting valid and necessary nested inductive types. They both fail to generate useful elimination principles for them. Rocq generates elimination principles that are too weak, failing to provide induction hypotheses for nested arguments. Lean, on the other hand, produces a "prettified" version of the elimination principle derived from the mutual encoding, which is not immediately usable and leaks the mutual encoding. In this work, we define a finer positivity condition for nested inductive types that enables us to modularly and syntactically ensure that a nested inductive type has a mutual encoding. Moreover, it rules out Rocq's wrongly accepted nested inductive types while accepting the useful ones rejected by Lean. Leveraging this new definition, we show how to define a "sparse" version of parametricity, and, thanks to it, useful elimination principles for nested inductive types.
Numerical instability or something more fundamental?
Áron Szabó
I report on what I have learned from a short project about numerical instability of eigenvector computation. After recalling some problems with floating point arithmetic, I will review exact real arithmetic from Bishop style constructive mathematics which fixes these problems. Armed with this, I present a short calculation about eigenvectors with an interesting conclusion.
Correct by Construction Design and its Challenges in Agda
Jaro Reinders
An overarching theme of my PhD has been correct by construction design. An example is intrinsic typing, which PLFA touts as saving about a golden ratio worth of lines of code. That sounds like a worthy goal, but it also generally requires more complicated language features which can be challenging to work with. I'll discuss these advantages and disadvantages in the context of my own work, namely the specification of context free languages and also to modular program transformations. Was the effort was worth it? Can we improve Agda to eliminate some of these challenges?
Setoid Heaven?
Yee-Jian Tan
... could possibly be achieved by removing the univalence axiom from Cubical Type Theory and instead postulating a conflicting axiom: the Uniqueness of Identity Proofs (UIP) postulate. Since univalence is proved in Cubical Type Theory from the so-called Glue Types, therefore, it is known that one can first remove the Glue Types (thus removing univalence) and then set-truncate all equalities (essentially assuming UIP), ŕ la XTT. The result is a “h-Set Cubical Type Theory” that retains features such as functional extensionality and QITs. However, in Cubical Agda, there are currently only two unsatisfying ways to achieve h-Set Cubical Type Theory. The first is to give up on the canonicity of the theory and simply postulate the UIP axiom, while the second way is to use a standard result stating “type formers preserve h-levels” to manually prove UIP for every defined type. The latter is, however, laborious work best suited for an automatic implementation by the proof assistant. In my master's internship, I analyse formulations of UIP and detail their computation rules for Cubical Agda, and evaluate their suitability for implementation. I also implemented a recently-merged variant of Cubical Agda without Glue, which is already compatible with postulated UIP, in anticipation of a future implementation of UIP in Cubical Agda.
Adventures in dependently typed programming - categorical cryptography edition
Andre Knispel
I will present some interesting problems and solutions I've encountered while formalising composable crypto in Agda.
agda2lambox
Lucas Escot
I will give a demo of the backend and provide some context on the project as a whole.

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.

Please indicate which days you plan to have lunch at the venue via this form.

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

You can find a hotel via Destination Angers or Angers Hotels, or via Booking.com or similar sites.

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. Also related to implementing double-checking of case trees, see #7628.
Implement local rewrite rules
Jesper Cockx
See https://github.com/TheoWinterhalter/local-comp
Generating websites from literate Agda (slides)
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, including versioning; this is also described in an `agda-stdlib` issue. Further documentation of this approach to website generation is available at https://pdmosses.github.io/agda-material/.
Improving the agda2lambox backend
Lucas Escot
This new backend enables compiling Agda to WASM/Rust/Elm by reusing the verified compilation infrastructure from MetaRocq/CertiCoq. The goal of this code sprint would be to tackle existing issues and figure out how to improve the backend.
New general-purpose open evaluator
András Kovács
Agda doesn't have any reasonably efficient evaluator which could be generally used in conversion or elaboration. `fastReduce` is reasonably fast, but still much slower than what should be possible, it can't go under binders and has the wrong value structure for general use. The plan is to do something simple first which can be used to refactor full instantiation and full normalization in classic NbE style.
Revive the Dedukti backend
Andreas and/or Jesper, hopefully Thiago
The Dedukti backend is currently not compiling due to API changes in Agda the library. Aarne Ranta wants to use it for his research of deformalizing mathematics so it would be great if we could restore it.
Cauchy (HoTT) reals for Cubical: design review & integration
Marcin Jan Turek‑Grzybowski (@marcinjangrzybowski), Lorenzo Molena (@LorenzoMolena)
Advance and scope PR #1182 “Book cauchy reals” for the Cubical library (HoTT Book §11.3), align interfaces with recent algebra/order work (e.g. OrderedCommRing, strict‑order reasoning, Nat/Int order instances, boolean builtins in Nat, faster /, %, gcd), and settle concrete design choices and next steps. Feedback or/and new contributors welcome!
AST navigation and interaction in emacs
Marcin Jan Turek-Grzybowski
I have working proof of concept, of AST based navigation in emacs, and enabling of using hole-specific emacs commands at AST nodes. I want to discuss that aproach, and feasibility of refactoring it into something mergable
Rewriting string diagrams
Andre Knispel
There is a relatively simple terminating & confluent rewriting system on string diagrams. We can use this to extract a solver for equality of morphisms in monoidal categories.
Code sprint title
Participants
short description
  • ...

Wrap-up notes

Unused import warnings

Andreas, Andras

Goal: implement new option -WUnusedImports that warns about imported names that are not used.

  • Sunday: started code sprint on the plane.
  • Monday: got it to compile, Andreas gives a demo.
  • Tuesday: Andreas made some small improvements, now supports public exports
  • Thursday: Andreas demos new features: warning on redundant opening of modules + on imported but unused names, nice interplay with no-qualified-instances (being an instance is not a proof of usage by default) + this also works on a per module base + and with renaming imports + overloading + module parameters, there are some subtle bugs
  • Saturday: Andreas got distracted by a related issue: you cannot use `using` and `renaming` on the same identifier in one open statement, but you can get the same effect with two open statements.

Agda2Dedukti backend

Andreas, Jesper

Agda2Lambox backend

Lucas, Carlos, Andre, Matthieu

  • Monday: Lucas fixed a bug, can now compile map on lists.
  • Monday: Carlos fixed Nix build, Andre is doing the same for the rest of the pipeline.
  • Monday: discussed about typed lambox, which requires inference of System F types.
  • Tuesday: Lucas fixed another bug.
  • Tuesday: Carlos started writing a typechecker for lambdabox.
  • Thursday: Carlos added type information in the syntax
  • Friday: Lucas is working to get type schemes to compile
  • Friday: Sylvain is working on name sanitation.
  • Saturday: Andre managed to compile one project to lambox.

HTML generation

Peter, Martin, Andre

  • Monday: discussed about potential new features.
  • Monday: Peter created an issue with his proposal for a new Make-based website generator (https://github.com/agda/agda-stdlib/issues/2893).
  • Tuesday: Peter is making a comparison of existing solutions for HTML generation and their features.
  • Thursday: there was a discussion in the afternoon, Peter will post a link to the presentation pdf. There was a pull request.
  • Friday: Andre gives a demo of the Agda-Material website generator (building on top of agda.nix).
  • Friday: Peter pushed a new PR that also accepts .lagda.md files.
  • Saturday: Marcin added more semantic nodes to the generated HTML with data from the abstract syntax that can be used by websites that integrate HTML generated by Agda

Open evaluator

Andras

  • Monday: started implementing some data types.
  • Tuesday: Andras is reviewing current implementation of slow and fast reduction, got distracted by potential improvements to rewrite rule reductions. Removed one traversal that seems to be unnecessary.
  • Thursday: András played around with nested inductive-inductive signatures

Rewrite rules

Jaro, Nathaniel

Quoting holes

Henry, Jesper

  • Monday: Henry started looking into the Agda internals.
  • Thursday: Henry makes an "anti-demo" with a simple example with a quoted hole; Marcin has a comment about holes and metavariables, the issue is that there is no way to quote a metavariable. Jesper: maybe a new type of opaque macro argument in the reflection API for holes? The id of syntactic metavariables are accessible. If change happens, it should be behind a flag.
  • Friday: Henry gives a demo of a modified Agda that removes the check for metas in macro arguments. Unfortunately the intended use case (an intro macro) does not work since macros cannot introduce new variables to the scope.
  • Saturday: There is a PR (https://github.com/agda/agda/pull/8235), under a flag `--quote-metas`. Working on adding some examples.

Cubical UIP

Yee-Jian

  • Monday: adding some builtins into Agda for generating proof terms
  • Thursday: Yee-Jian implements the composition rules for Pi
  • Friday: Yee-Jian is trying to debug the Pi computation rule. Something is happening.
  • Saturday: Yee-Jian is still debugging, no progress to report.

Cauchy reals in Cubical Agda

Marcin, Lorenzo

  • Monday: started working on this, rebased previous work on current master.
  • Tuesday: Marcin and Lorenzo discussed what would be a realistic subset to clean up in this week. Marcin will fix solver for rationals, Lorenzo will work on getting the decimal expansion of e to compute (fast enough).
  • Thursday: Marcin and Lorenzo specialised the cubical ring solver to fast integers, could automatise ~150 lemmas, there is potential for more. Lorenzo worked on fast integers and the convergence of the series defining the exponential map, much faster than the slow definition
  • Friday: Lorenzo is working to parametrize the reals over the ring that is used as the base (WIP).
  • Saturday: Lorenzo and Marcin cleaned up 5000 lines of code to avoid lossy-unification.

Interactive AST-based navigation

Marcin, Andras

  • Monday: Marcin gives a demo. You can navigate the AST and get the type and value of each subexpression. Eventually the goal would be to call an arbitrary macro on any subexpression interactively. Code is messy, but draft PR is submitted.
  • Tuesday: Marcin is slowly cleaning up the PR. Andras helped to get a small part merged into master.
  • Thursday: Marcin worked out a way to color places where hidden arguments have been added. Performance testing is planned for Friday.
  • Saturday: Marcin added nodes for printing the values of hidden arguments. Discussed with Andreas about splitting the changes into smaller PRs so they can be integrated into Agda.

Agda setup action

Updating the Agda parametricity library

A practical type to describe wire composition

  • Thursday: Andre demos a partial solution based on an idea of Andreas
  • Saturday: Andre had an idea but hasn't tried it yet.

New Agda webpage

Synthetic domains and denotational semantics

  • Thursday: Peter made some progress with András, Jesper found a bug (and reported it)
  • Friday: Peter ran into a roadblock: there is interference between the rewrite rules and the types when working with nested function domains.
  • Saturday: The roadblock was fixed, everything seems to work well.

Adding sort & erasure information to treeless syntax

  • Thursday: Jesper has been working on issue 5315 about dropping arguments that have a 0 on them in the GHC backend
  • Saturday: Jesper made a PR that (partially) fixes #5315 (https://github.com/agda/agda/pull/8239).

Detecting assumptions

Vojta

  • Friday: Vojta has implemented an ASSUMPTIONS pragma that prints all the postulates that are used by a definition. Detected an unwanted dependency on funext in agda-unimath. Final goal: declaring an explicit list of allowed postulates.
  • Saturday: Vojta is working to support more syntactic forms. It is now also looking into types of definitions.

STG Backend

Jaro, Sylvain

  • Wednesday: Jaro started to build a new backend based on Jesper's old Scheme backend.
  • Friday: Sylvain helped Jaro to deal with variables and data constructors, there is a plan now.
  • Saturday: Jaro made progress. Implementing case splits and data constructors. The main thing left is dealing with names. Unfortunately no demo yet.

Agda2hs

Andreas, Jesper, Copilot

Adding copy-avoiding strict substitution

Andras

  • Friday: Andras tried to add copy-avoiding strict substitution to metavariable solutions but is getting internal errors.
  • Saturday: Andras confirmed that copying is indeed avoided. At the moment it seems to not be worth it in terms of performance.

Display pragmas

Package management

  • Saturday: Andre presents an example of a basic package management layer on top of Agda.nix Link

Documentation

Edit | History | Recent Changes (all) | Search
Page last modified on December 02, 2025, at 12:15 pm
Powered by PmWiki