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.

TuesdayMay 308-10 (10-12)Welcome + Planning of code sprints8103 (10-17)
  10.00 (12.00)Codesprint 1 "irrelevant instances discussion"Zoom breakout 1
  12.00 (14.00)Codesprint 4 "TC reader"Zoom breakout 4
  13.00 (15.00)Codesprint 5 "agda2hs"Zoom breakout 5
  14.00 (16.00)Codesprint 9 "standard library"Zoom breakout 9
WednesdayMay 412.00 (14.00)Codesprint 7 "refine"Zoom breakout 7
  14-15 (16-17)Talk by Andre Knispel:8103 (12-17)
   Human and machine-readable models
   of state machines for the Cardano ledger
ThursdayMay 507.30 (09.30)Codesprint 2 "agda2scheme"Zoom, EDIT 8103
  13.00 (15.00)Codesprint 5 "agda2hs"Zoom, EDIT 5128
  14-15 (16-17)Daily meeting8103
FridayMay 608-09 (10-11)Daily meeting6128
  09-10 (11-12)Codesprint ?Zoom, 6128
  13-15 (15-17)Codesprint ?Zoom, 6128
  17.00 (19.00)PubRotary pub, Gbg
 
MondayMay 908-09 (10-11)Talk by Matthew Daggitt:6128 (10-17)
 Verifying ML-enhanced systems in Agda
 - keeping the car on the road
  09-10 (11-12)Daily meeting6128
TuesdayMay 1014-15 (16-17)Daily meeting6128 (14.30-17.30)
WednesdayMay 1108-09 (10-11)Daily meeting6128 (10-13)
  09-12 (11-14)Codesprint agda2hs bugfixesZoom
ThursdayMay 1208-09 (10-11)Talk by Josh Ko followed by discussion6128 (10-15)
 led by Liang-Ting Chen and Tzu-Chi Lin:
 Reflections on datatype-generic programming
FridayMay 1314-15 (16-17)Wrap-up6128 (10-17)

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.

Oskar ErikssonUTC+2
Julian MendezUTC+2
Matthew DaggittUTC+1
Jesper CockxUTC+2
John LeoUTC-7
Lucas EscotUTC+2
William DeMeoUTC-4
Felix CherubiniUTC+2
Liang-Ting ChenUTC+8
Wen KokkeUTC+1
Fahad F. AlhabardiUTC+1
Nils Anders DanielssonUTC+2
Tzu-Chi LinUTC+8
Guillaume AllaisUTC+1
Orestis MelkonianUTC+1
Andre KnispelUTC+1
Josh KoUTC+8
Marcin Jan Turek-GrzybowskiUTC+2
Alasdair HillUTC+1
Ulf NorellUTC+2
Andreas AbelUTC+2
Evan CavalloUTC+2
Fredrik Nordvall ForsbergUTC+1
Nicolai KrausUTC+1
Matthias HutzlerUTC+2
Shin-Cheng MuUTC+8
James ChapmanUTC+1
Anton SetzerUTC+1

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)
Page last modified on May 10, 2022, at 07:48 PM
Powered by PmWiki