Main /
\ Main

Agda Implementors' Meeting XLII

List of Agda meetings

The forty-second Agda Implementors' Meeting (AIM XLII) took place in Leuven, Belgium from 2026-04-13 to 2026-04-18 (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.

Location

Leuven, Belgium. More information on the location.

Zulip stream

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

Food

There will be sandwiches at noon, some snacks & fruit, and coffee.

Program

Mon Apr 13

  • 9h30 Welcome, introductions, finalizing schedule
  • 10h30 Coffee break
  • 11h00 Talks
    • Lawrence: Programming in Agda
    • Code sprint
  • 12h30 Lunch
  • 14h00
  • 15h30 Coffee break
  • 16h00 Code sprints
  • 17h30 Wrap-up meeting

Tue Apr 14

  • 9h30 Talks
    • 9h30 Short industry talk: Faulhorn Labs
    • 9h45 Short industry talk: IOG
    • 10h00 Antoine VM: Agda --bridges: internal binary parametricity with a substructural type system
  • 10h30 Coffee break
  • 11h00 Discussion: A strategy for non-standard TT contributions to Agda
  • 12h30 Lunch
  • 14h00 Discussion: LLMs and Agda (Part 1)
  • 15h30 Coffee break
  • 16h00 Code sprints
  • 17h30 Wrap-up meeting

Wed Apr 15

  • 9h30 Talks
    • 9h40 Balázs: A second*-order model of dependent pattern matching
    • 10h45 András: Haskell Performance of Agda Development
  • 12h?? Lunch
  • 14h00 Discussion: LLMs and Agda (Part 2)
  • 15h30 Coffee break
  • 16h00 Code sprints
  • 17h30 Wrap-up meeting

Thu Apr 16

Activity (draft):

  • 14h00 Start at Sint-Kwintenskerk, Naamsestraat, Leuven (there's a bus stop by the same name)
  • The city loop of this walk
  • Depending on how much more we want to walk:
    • walk to Abdij van Park / Park Abbey
    • walk to Kasteelpark Arenberg
    • walk to Egenhovenbos
    • maybe continue to Heverleebos
  • So we may not end up at the starting point, but there are buses!

Fri Apr 17

  • 9h30 Talks
  • 11h00 Coffee break
  • 11h30 Discussion: Modalities in Agda
  • 12h30 Lunch
  • 14h00 Code sprints
  • 15h30 Coffee break
  • 16h00 Code sprints
  • 17h30 Wrap-up meeting

Sat Apr 18

  • 9h30 Talks / Code sprints
    • 9h30 Peter Mosses: Website generation
  • 10h30 Coffee break
  • 11h00 Talks / Code sprints
    • Demo by Nathaniel Burke: Smart with
    • Demo by Yee-Jian Tan: Cubical-UIP
  • 12h30 Lunch
  • 14h00 Week wrap-up
  • 15h30 Coffee break
  • 16h00 Oh no, before you go, let's sort out this one thing together!

Registration

Registering for the meeting is free but mandatory. There is a soft registration deadline on March 8, 2026. (This has passed, but you can still register.) 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 Andreas Nuyts. 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: Andreas Nuyts
Subject: Registration for AIM XLII
  • 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

  • Andreas Nuyts (KU Leuven)
  • Yee-Jian Tan (KU Leuven)
  • Lawrence Chonavel (Utrecht University)
  • Jesper Cockx (TU Delft) - all week except Thursday
  • András Kovács (University of Gothenburg & Chalmers University of Technology)
  • Andreas Abel (University of Gothenburg & Chalmers University of Technology)
  • Vojta Štěpančík (INRIA)
  • Balázs Kőműves (Faulhorn Labs)
  • Ziyang Liu (IOG)
  • Nathaniel Burke (TU Delft)
  • Sam Toth (University of Nottingham)
  • Antoine Van Muylder (KU Leuven)
  • Jaro Reinders (TU Delft)
  • Peter Mosses (TU Delft)
  • Antoine Kinable (ULičge) - Monday and maybe second half of the week
  • 2 anonymous

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.

A second*-order model of dependent pattern matching
Balázs Kőműves
While trying to implement a dependently typed language similar to Agda, we ran into all kinds of predictable issues; this led into a prolonged exercise in the meta-theory of type theories. One of the most confusing puzzle pieces is dependent pattern matching, so it's a natural and desired target for formalization. Here we try to do that, using higher-order abstract syntax as the starting point. I'll present my interpretation of the work done by Péter Diviánszky. This also has a large overlap with the work of Jesper Cockx (in particular "Agda core" and "Unifiers as Equivalences").
Agda --bridges: internal binary parametricity with a substructural type system
Antoine Van Muylder
TBA
Haskell Performance of Agda Development
András Kovács
Short abstract
Recap: What kind of agentic proving is currently being done at Chalmers
Andreas Abel
Short abstract

Excursion

Leuven city walk.

Discussions

Discussion: The current state of usability of Agda as a programming language
Participants
This quote from an HN comment is very interesting, and is why I propose this discussion topic: "I code real life programs in Agda. Some part of my server and my tools are in Agda. One time I was in #haskell freenode IRC channels and people started acting out as if I'm some crazy person. Agda has seemless integration with Haskell. There is almost no friction writing 20% of your program in Haskell (unsafe) and 80% in Agda (safer). I personally believe, agda is an *excellent* programming language. It's stdlib is good, concepts and construct are very well-thought out, it's very safe and works surprisingly well. I've been programming in agda for years and almost never had issue implementing anything *even though* it's not Turing complete. Using sized types you can prove most sane things to terminate anyway. And if you really need infinite loops (say, you're implementing an interpreter of a Turing complete language) then you have many options: (1) disable termination checking for a single function (2) use Haskell to implement a single function (3) use Rust, C, C++ etc to implement a function then with GHC ffi link it to agda."
Discussion: Modalities in Agda
Proposed by: Sam Toth
Participants
I would be interested in discussing both the current state of modalities in Agda and thinking about unifying the existing modalities or extending and Agda with more modal features. My personal motivations are around the formalisation of simplicial/triangulated type theory where at least having flat, sharp and op modalities seems quite important for practical formalisation. There are also other more exotic modalities such as the twisted arrow modality and the ‘amazing right adjoint modality’ which are used in the literature around STT. I would be interested in hearing other people motivations for different modal theories, especially ones which might fall outside of the framework of MTT or Shulman's multimodal-adjoint type theory.
Discussion: LLMs and Agda
Participants
See PR 8456
Discussion: A strategy for non-standard TT contributions to Agda
Proposed by: Andreas Nuyts
Participants
Agda is very suitable as a substrate language to which we can add proof-of-concept or even mature support for non-standard type systems under active research. It is quite understandable that not all of these make it into the master branch. Still, I think it would be nice to have a discussion on how we can make such extensions more easily digestible to the master-branch, and otherwise if we can find a better fate for them than bitrot. Is a notion of plug-ins for Agda imaginable?
Code sprint
Participants
Short abstract

Code sprints + wrap-up notes

  • Unused imports (Andreas A, ?)
  • Optimizing heterogeneous conversion checking / anti-unification (András, Jesper, help wanted)
  • Agda issue #5810: subject reduction with Setω (Jesper, András, maybe Andreas N?)
    • Monday: Jesper added boolean flag to Pi type internal syntax, started to update elaboration to set it.
    • Tuesday: Jesper added surface syntax @leveldep (subject to bikeshedding) and fixed one de Bruijn bug.
    • Wednesday: Jesper: no progress

Open question: how to infer @leveldep annotations for module parameters?

  • Agda2hs issue #126: public exports & imports (Jesper, ?)
  • Local rewrite rules / smart-with (Nathaniel, Yee-Jian, ?)
    • Monday: Nathaniel added a flag, fixing bugs with weird interactions between flags
    • Tuesday: working on making smart rewrite work, hitting many bugs and fixing them
    • Wednesday: nothing.
    • Friday: trying to understand scoping in `stripWithClausePatterns`
    • Saturday: fixed scope error in `stripWithClausePatterns`
  • Website generation (Peter, ?)
    • Monday: slow progress on refactoring the Makefile
    • Tuesday: finished refactoring the Makefile, taking a serious look at CI workflow for stdlib.
    • Wednesday: looked at current std-lib CI, seems possible to generate a website
    • Friday: generated websites available in Peter's fork, debugged github actions (Peter, Andreas)
    • Saturday: - released v0.0 of the Agda Material, works with stdlib and TypeTopology; - working on a common submodule that can be imported; - working on addressing garbage links on landing page.
  • Forester backend (Sam, ?)
    • Friday: fixed a bug linking form HTML to literate files & debugged more (Sam)
  • Cubical UIP (Yee-Jian, Nathaniel, ?)
    • Wednesday: demo WIP
    • Saturday: trying to do this with rewrite rules, filed #8519, Nathaniel is working on this
  • Issue #8100: level normalisation (Andreas, Jesper)
    • Monday: Andreas wrote some property tests for the levelLub function (no bugs found)
    • Tuesday: PR got merged. #8100 got fixed by fiat (but could perhaps be improved by using inlining on the level primitives).
  • Optimization of Agda (András)
    • Monday: András optimized metavariable occurs checking, gets 1.5% speedup on TypeTopology.
    • Tuesday: now the optimization passes all tests, because Andras changed the tests, the old version was buggy.
    • Wednesday: PR made, seems to work.
  • Experiments with --guarded (Sam, ?)
    • Monday: trying to generalize it to other modalities. Enabled datatypes for LockUniv.
    • Wednesday: considering switch from affine to linear
  • "Print assumptions" command (Vojta)
    • Monday: bringing the PR from previous Agda meeting into a reviewable state
    • Tuesday: factored out a small PR to Agda mode to have colored output in debug printing, still cleaning up code for "print assumptions".
    • Wednesday: mismatch between CI and local test run
    • Friday: better core generation
    • Saturday: code is now way uglier, plus it doesn't work
  • De-Makefile-ifying the interaction test suite
    • Monday: mostly done, currently debugging
    • Tuesday: see above.
    • Wednesday: 70% of tests finished
    • Friday: PR #8513
  • Compiling with GHC 9.14 (Andreas A)
    • Saturday: Success
  • Removing unused generalized records from interface files (András)
    • Saturday: This happened.

Acknowledgements

This event is supported by the Research Fund KU Leuven and KU Leuven Internal Funds. The organizers also wish to thank the DistriNet Business Office and the departmental support team at KU Leuven, dept. of Computer Science for their valuable support.

Edit | History | Recent Changes (all) | Search
Page last modified on April 20, 2026, at 12:42 pm
Powered by PmWiki