Agda Implementors' Meeting XXXV

The thirty-fifth Agda Implementors' Meeting will take place between 2022-05-03 and 2022-05-13. Everyone who uses Agda is invited to attend.

Due to the current pandemic the meeting will be held online. 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

2022-04-26

Soft deadline for registration

2022-04-26 to 2022-05-02

People can express interest in code sprints

2021-05-03 to 2021-05-13

AIM XXXV

Registration

You register for the meeting by entering your name below. Registration is not compulsory. If you would like to give a talk or propose a discussion, please send an email to Oskar. To propose a code sprint, please add this to the list below.

Links and Technology

All talks and discussions can be attended through Zoom (meeting id 63108860164, password 1234, same link for all talks).

Similarly 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-xxxv stream which will contain all the information related to the meeting! To join Zulip from an app see the Zulip website.

Programme

Times are given in UTC (CEST).
For people in Gothenburg, rooms have been booked, see room numbers below.

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.

Talks and discussions

• Andre Knispel: Human and machine-readable models of state machines for the Cardano ledger
  The Cardano Ledger is a very large state machine that is formally specified on paper. Turning this specification into a machine checked model has many benefits, but it comes with many constraints. Some of them come from the paper specification that we want to maintain, but there are also some further constraints imposed by the purposes we have for this model.
  In this talk, I'll discuss the problems we are trying to solve with this model, the reasons why we chose Agda over other alternatives, how we are using some of Agda's features and what new problems we ran into.
• Matthew Daggitt: Verifying ML-enhanced systems in Agda
  Suppose you have a 20,000 node neural network that controls a car on the road. How can you formally prove that the car will never leave the road? Any proof will likely involve both automatic reasoning about the neural network and deductive reasoning about the state space. In this talk I will describe our new tool "Vehicle" for constructing such proofs. Problems with this approach include that a 20,000 node network isn't even easily representable in Agda and that naively integrating an external neural network solver that takes minutes, hours or even days to complete will seriously disrupt Agda's interactive mode.
• Josh Ko, Liang-Ting Chen and Tzu-Chi Lin: Reflections on datatype-generic programming
  A dependently typed language like Agda is said to be a natural platform for datatype-generic programming (DGP), with which we can compute derived functions and even datatypes for a wide class of datatypes. However, DGP is not as popular as it should be, and we see repetitive code in, for example, Data.List.Relation.Unary.Any, Data.Vec.Relation.Unary.Any, Data.Maybe.Relation.Unary.Any, Data.Tree.AVL.Indexed.Relation.Unary.Any, etc in Agda’s standard library. More generally, the use of datatypes with intrinsic properties makes the situation even messier than other non-dependently typed languages.
  In this session, we will briefly demonstrate a different approach to DGP. Instead of operating on only those datatypes that are instances of a fixed-point datatype, we extend Agda’s reflection mechanism with an experimental syntax and new reflection APIs so that derived datatypes can be created natively by invoking a macro to reify datatype descriptions; these descriptions are usually computed from descriptions of existing datatypes, and the latter can also be obtained by invoking another macro.
  With DGP serving as a motivation, we would like to invite the participants to think over possible improvements to the current design of Agda’s reflection framework and make metaprogramming more powerful and easier to use in Agda.

Code sprint proposals

1. Modify the behaviour of instance search to admit non-unique solutions when trying to solve for irrelevant instances, which is strongly desirable for the release of v2.0 of the standard library (see issue #5494).

• Participants: Matthew Daggitt, ???
• Initial discussion - Irrelevant Instances Zoom breakout room 11am (UK time) Monday 3rd of May.

2. Hacking on the Agda2Scheme backend (see https://github.com/jespercockx/agda2scheme)

3. Alter the standard library ring solver to work with abstract rings (see issue #1116).

• Participants: Matthew Daggitt, Felix Cherubini, ???

4. Turn the TC monad into a reader/state monad, for an easier and more consistent interface. See issue #5873.

• Initial discussion: 1pm UK time (3rd May) in Zoom breakout room

5. Write a program using agda2hs, prove properties about it and compile it to Haskell.

• Initial discussion: 2pm UK time (3rd May) in Zoom breakout room

6. Add the ability to mark external system calls as "volatile" issue #5859).

• Participants: Matthew Daggitt, Wen Kokke(?), ???
• Initial discussion: 1pm UK time Thursday, 5th May in Zoom breakout room

7. Modify the behavior of Refine (C-c C-r) command in interactive agda mode. (Marcin Jan Turek-Grzybowski) https://docs.google.com/document/d/1VqtjOrrDlz-cNLi8eHBwlanuKZ75TrvB7_cVerIfcdw

• Participants: Marcin, Andreas, ...
• Initial discussion: 1pm UK time (4rd May Wednesday, in Zoom breakout room 7)

8. Steal some ideas from smalltt & Idris (#5797, #3094). E.g. glued term representation.

• Participants: Ulf, Nisse, Guillaume, ...
• Initial discussion: 10.15am UK time (3rd May)

9. Standard library affairs

• Participants: Matthew, ...
• Initial discussion: 3pm UK time (3rd May)