If you're here for AIM XXXIV in June 2021, please go to https://wiki.portal.chalmers.se/agda/Main/AIMXXXIV
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
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. Don't forget to also join the aim-xxxiii stream which will contain all the information related to the meeting! 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.
- 10-11: Introduction
- 11-12: Planning of discussions and code sprints
- 15-16: Talk by Wen Kokke: "Schmitty the Solver"
- 10-11: Talk by Jesper Cockx: "Agda Core: Where do we come from and where do we go?" (slides)
- 11-11:30: Wrap-up meeting
- 15:00: Discussion: Improving interoperability of the libraries
- 15-16: Talk by Jacques Carette and Jason Hu: "The new categories library for Agda"
16-16:3016:30-17: Wrap-up meeting
- 10-11: Talk by Ulf Norell: "Programming with Universes for Fun and Profit"
1112-13: Code sprint on Agda Core
- 13: A discussion about the structure identity principle (zoom)
- 14-15: Discussion (lead by Víctor López Juan): Twin types in Agda
- 11-12: Talk+Discussion lead by Thorsten Altenkirch: "Coinduction in cubical agda"
- 15-16: Wrap-up meeting
- 16-: Social event: AIM XXXIII Pub
- 14 - ?: Social event: Virtual Excursion (TBA).
- 10-11: Talk by Stefania Damato: "Constructing Simple and Mutual Inductive Types in Agda"
- 11-12: Discussion about Sized Types
- 15-16: Talk by James Chapman: "Higher Assurance Haskell: Using Agda to model and test a Haskell program (experience report)"
- 16-16:30: Wrap-up meeting
- 17:30-21: Social event: Dungeons & Chickens (organized by Jesper Cockx)
- 10-11: Talk by Nicolai Kraus: "Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it?"
- 13-15: Work on Compiling Agda to Readable Haskell code sprint
- 11-12: Continued discussion of sized types, hopefully culminating in implementation sketch
- There will be no talks this day, but attendants are encouraged to join the talks at SPLS. The code sprints and discussions will continue as normal.
- 10-11: Talk by Johannes Schipp von Branitz: "Displayed Univalent Reflexive Graphs in CTT"
- 11-11:30: Wrap-up meeting
- 15:30-17: (Not part of AIM but likely of interest.) Ambrus Kaposi: "Quotient inductive-inductive types and higher friends" HoTT Electronic Seminar
- 11-12: Talk by Musa Al-Hassy: "Do-it-yourself Module Systems: Unbundling on the fly and mechanically obtaining term types from theories"
- 12-14: Final wrap-up meeting
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|
|Marcin Jan Grzybowski||UTC+2|
|Nils Anders Danielsson||UTC+2|
|Marcus Christian Lehmann||UTC+2|
|Johannes Schipp von Branitz||UTC+2|
|Jakob von Raumer||UTC+2|
|Tesla Ice Zhang||UTC+8|
Talk and discussion proposals
- 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!
- Jesper Cockx: Agda Core: Where do we come from and where do we go? A recurring question people have about Agda is "why doesn't it have a proper core language?" In this talk, I'll discuss the current state of the internal double-checker of Agda, past attempts at formalizing more of Agda's theory (see https://github.com/agda/agda-spec), and how we could move towards having a proper core language for Agda in the future.
- Jacques Carette and Jason Hu: The new categories library for Agda Details TBA.
- Ulf Norell: Programming with Universes for Fun and Profit To write tactics or other meta-programs in Agda you need to manipulate reflected syntax--an Agda representation of the internal syntax of Agda itself. Its definition consists of a handful of mutually recursive datatypes representing terms, patterns, sorts, etc, and defining functions over these can be a bit awkward. In this talk I will show you some infrastructure for working with reflected syntax, and how using universes can make everything much nicer.
- Víctor López Juan: Twin types in Agda A discussion on how to add twin types to the Agda typechecker (see https://dl.acm.org/doi/abs/10.1145/3406089.3409030 for the theory, and https://github.com/agda/agda/pull/4605 for WIP code)
- Thorsten Altenkirch : Coinduction in cubical agda I want to discuss some issues with doing coinduction in cubical agda.
- Stefania Damato: Constructing Simple and Mutual Inductive Types in Agda A description of work done for my master's thesis, involving the construction of a framework in which we can express simple and mutual inductive types, and a starting point for a reduction from these types to W-types.
- Nicolai Kraus: Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it? 2LTT is a small extension of dependent type theory and allows us to reason about strict (a.k.a. judgmental/definitional) equality semi-internally. I briefly want to talk about how this works, what one can do with it, why one would want to do that, and what (from my point of view) is still missing on the theoretical side. I only need 15min or so for the talk, but I hope we can afterward discuss whether other projects could benefit as well from 2LTT and what people's requirements would be.
- Johannes Schipp von Branitz: Displayed Univalent Reflexive Graphs in CTT
A univalent reflexive graph (URG) on a type is a reflexive binary relation such that the canonical map
idToRelis an equivalence. A displayed URG over a URG roughly consists of a type family where each fiber carries the structure of a URG, but the fields depend on the URG on the base type. A DURG induces a URG on the total type of its underlying type family, giving rise to a characterization of the identity types of the total type. I used them to prove the equivalence of strict 2-groups and crossed modules, but I will put the focus of the talk on the meta-theory of DURGs. The code can be found at #435 . My thesis is available here.
- Nils Anders Danielsson: Making different libraries interoperable and/or merging them Explanation.
- James Chapman: Higher Assurance Haskell: Using Agda to model and test a Haskell program (experience report) At IOHK we have a core language based on System F omega mu for our smart contract platform Plutus. We have an intrinsically typed implementation of an interpreter and type checker for this language in Agda. We compile the interpreter to Haskell and make use of the same Haskell libraries as the production implementation and also borrow the production parser and pretty printer. The Haskell executable serves as a reference implementation which we can test the production implementation against, on hand written examples, and on NEAT generated System F omega mu terms due to work by Wen Kokke. I will describe some details of the project and the experience of using Agda for this project and some thoughts on future applications.
- Musa Al-Hassy: Unbundling on the fly and mechanically obtaining term types from theories We show how a bit of reflection can be used to achieve on the fly unbundling to lift record fields to the type level as parameters, and we use monadic do-notation to make the resulting setup practical and pragmatic for experimentation. It is well known in the folklore that record types are contexts (i.e., sequences of name-type pairs), we go on to show that termtypes (GADTs) are also contexts. Moreover, since records and termtypes are both contexts, we show how to derive the latter from the former mechanically via a macro; e.g., we mechanically ask for the termtype of dynamic systems, monoids, pointed sets, collections and find the results to be that of the natural numbers, tree skeletons, the maybe type, and the list type. Surprisingly, the entire development is under 300 lines of Agda. Project webpage: https://alhassy.github.io/next-700-module-systems/
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 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. People who are interested in taking part in the code sprint: Anders, Marcus, Max, Martin, Marcin, Ulrik ...
- Jesper Cockx: More control over reduction for interaction & reflection Currently the Agda typechecker features only two main modes of reducing a term: either reducing it to weak-head normal form, or fully normalizing it. However, during interactive use it would often be nice to reduce just calls to a specific function, or to limit the set of allowed reductions in other ways. This code sprint will be about implementing the core mechanism for this in the Agda typechecker, and binding it to the reflection interface so it can be used in (both compile-time and edit-time) macros. People who are interested in taking part in the code sprint: Jesper, John, Kyle, Artem,...
- Arjen Rouvoet (proposing, not an expert): Distributing Agda I would like to discuss the channels via which we distribute Agda. It seems we heavily rely on cabal/stack for typical installations, which are not package managers and at least in my personal experience break for a variety of reasons, all the time. Is it feasible to produce binary distributions of Agda? People interested: Andreas
- James Chapman: Compiling to readable Haskell I would like to investigate creating a new compiler backend for Agda aimed at verifying Haskell programs that generates readable Haskell from a restricted subset of Agda. The intended use case would be using Agda to verify a key component in a Haskell project and then generating readable Haskell that can be easily integrated with the Haskell project. People interested: James, Andreas, Ulf
- Manuel Bärenz: Fixing sized types Sized types have bugs where you can prove bottom, essentially making them inconsistent or `--unsafe`, e.g. https://github.com/agda/agda/issues/2820. The very least that should be done is marking them as unsafe. But ideally, we'd fix the implementation. I (Manuel) don't know what the right theory is, but if experienced people can offer some guidance what the right approach is, I/we can attempt to fix it. The first step would be to meet and work out a sound theory on a virtual whiteboard. Then we can discuss implementation. People interested: Manuel, Andreas, Nisse, Andrea
- Ulf Norell: Quasiquoting for reflection Working with reflected syntax can be quite painful. The goal of this sprint is not to implement full quasi-quoting, but rather investigate how far we can get with the existing machinery and clever libraries, and if there are any low hanging fruits in terms of extensions that could make our lives easier. People interested: Ulf, Manuel
- Nils Anders Danielsson: Improving erasure support People interested: Nisse
- Johannes von Branitz: Displayed Univalent Reflexive Graphs People interested: Johannes, Ulrik
- Manuel Bärenz: Use more instances in the standard library It would be nice if instances like Show and Eq were implemented more in the standard library. They are fairly prevalent in `agda-prelude`, so maybe it is time to merge the prelude into the standard library, and refactor the latter accordingly. People interested: Manuel
- Proposer: Title Description People who are interested in taking part in the code sprint: ...
- The Agda pub: Bring your own fancy beer and/or delicious pub food for a nice evening, and discuss whatever's on your mind!
- Virtual excursion: Hike or bike to a local beauty spot, share your pictures, and join us on Zoom for a relaxing morning/afternoon.
- Dungeons & Chickens: In which I (Jesper) will host a game of Dungeons & Dragons on Discord for anyone who wants to join, no previous experience required. This game will be suitable for 1st level characters and might feature two very angry chickens named Agda and Coq.