Agda Implementors' Meeting XXXIII

The thirty-third Agda Implementors' Meeting will take place between 2020-10-12 and 2020-10-23. Everyone who uses Agda is invited to attend.

Due to the current pandemic the meeting will be held online. It will be held over two weeks instead of one, but each day might be less intense than in previous meetings. We will try to accommodate participants from different time zones. Please indicate at what times of the day that you are available when registering.

Important dates

Soft deadline for registration
2020-10-05 to 2020-10-11
People can express interest in code sprints
2020-10-12 to 2020-10-23 (weekdays only)


You register for the meeting by sending an email to Jesper, or by entering your name below. Registration is not compulsory. If you would like to give a talk or propose a discussion or code sprint, please include this in your registration email.

Links and Technology

Talks and discussions will be held via Zoom or other channels depending on the preferences of the speaker. Links to Zoom or similar systems can be found in the programme below.

In contrast to the previous online Agda meeting, all code sprints and other text-based communication will be held via Zulip, which can be joined here. To join Zulip from an app see the Zulip website.


Note: UTC is used for dates and times.

One hour has been scheduled for talks and discussions. However, note that it is fine to give a shorter talk, and discussions might take more than one hour if there is a lot of interest in them.


Note: the will be no talks scheduled on October the 21st, but attendants are encouraged to join the talks at SPLS. The code sprints and discussions will continue as normal.

Registered participants

If you are not working during "normal business hours" you may want to give a time zone that differs from the one in effect at your physical location.

NameTime zone
Jesper CockxUTC+2
John LeoUTC-7
Wen KokkeUTC+1
Swaraj DashUTC+1
Jorge Blázquez SaboridoUTC+2
April GonçalvesUTC+1
Manuel BärenzUTC+2
David BanasUTC-7
Jacques CaretteUTC-4
Conal ElliottUTC-7
Anders MörtbergUTC+2

Talk proposals

List talk proposals here.

  • Wen Kokke: Schmitty the Solver
    I recently published an Agda library called Schmitty, which provides flexible bindings between Agda and SMT-LIB solvers. In this talk, I'll go over the basic design of Schmitty, and propose several small extensions that would make excellent code sprints!
  • Proposer: Title

Code sprint proposals

List code sprint proposals here.

  • Wen Kokke: Schmitty the Solver
    Schmitty provides flexible bindings between Agda and SMT-LIB solvers. There's a large number of possible extensions for Schmitty to make her even more useful! Right now, Schmitty supports the core theory, i.e., propositional logic, as well as integer arithmetic linked to Agda integers, and real arithmetic linked to Agda floats. However, the SMT-LIB standard offers so many more possibilities!
    • Add backends for other SMT-LIB compliant solvers (easy);
    • Add a testing framework which supports negative tests (easy);
    • Add theory of real arithmetic linked to Agda rational numbers (easy);
    • Add theory of floating-point numbers linked to Agda floats (easy);
    • Add theory of strings linked to Agda strings (easy);
    • Add theory of sequences linked to Agda lists (moderate);
    • Add theory of uninterpreted functions and constants linked to Agda names (moderate);
    • Add theory of regular expressions linked to gallais/aGdaREP (moderate);
    • Add theory of algebraic datatypes linked to Agda datatypes (moderate);
    • Add theory of arrays linked to an axiomatisation of Haskell arrays (moderate);
    • Add support for combined theories (moderate);
    • Add support for logic declarations (moderate);
    • Add proof reconstruction for SAT using Kanso.SatSolver (moderate);
    • Add proof reconstruction for Z3 proofs (cf. Proof Reconstruction for Z3 in Isabelle/HOL) (hard).
    People who are interested in taking part in the code sprint: Wen, Jorge, Manuel, ...
  • Anders Mörtberg: Cubical Agda and the agda/cubical library
    Hopefully other agda/cubical contributors can attend so that we can fix many of the issues and merge some of the open PRs.
  • Proposer: Title
    People who are interested in taking part in the code sprint: ...

Wrap up reports

Page last modified on September 24, 2020, at 07:42 AM
Powered by PmWiki