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.
- 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)
- AIM XXXIII
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.
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.
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.
|Jorge Blázquez Saborido||UTC+2|
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 Explanation.
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).
- 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 Description People who are interested in taking part in the code sprint: ...