CakeML Developers Meeting 2019
A discussion about the future development and use of CakeML
Date: 13-14 May 2019
Venue: EDIT room Analysen, Chalmers, Sweden — How to find the venue
Purpose
This meeting aims to bring together as many people as possible working on or using CakeML. CakeML is a distributed project with developers and users across at least 7 sites (3 continents): Sydney, Canberra, Chalmers, MPI, TUM, Kent, CMU, Uppsala, KTH. As such, it is beneficial for developers and users to once in a while meet face-to-face to get to know each other, re-cap what has been going on, and to create a common vision for the future of the project.
Attending
There is no registration or registration fee. However, people who want to take part in the social event on Monday 13 (Bouelbar) must let Magnus know that they are coming.
Format
There is a programme with presentations (see below). The idea is that each presentation leaves time for discussions. Demos are highly encouraged and plenty of prior knowledge of CakeML can be assumed of the audience when preparing presentations. Presentations can be anything from proper slides to sketching something in a text editor. Interactive presentations are highly encouraged.
The programme below was put together so that everyone gets to know each other and each other's work on day 1; and day 2 is left more open with time for hacking and talks on new/recent projects. Presentations may be moved around on the day in case an item requires less time than exepcted.
Day 1 — Monday 13 May 2019 — "What's new?"
09:00
- Coffee/tea outside meeting room
09:15 - 10:30
- general introduction — Magnus Myreen and Ramana Kumar (10 min)
- everyone introduces themselves (and their site) (25 min)
- HOL: where will it develop — Michael Norrish (20 min)
- how bootstrap was sped up — Thomas Sewell (15 min)
Break
10:50 - 12:00
- ad hoc overloading in Candle — Arve Gengelbach (15 min)
- latest on Candle — Oskar Abrahamsson (15 min)
- verified CPU that can run CakeML code — Andreas Lööw (15 min)
- news on choreographies — Alejandro Gomez (10 min)
- CakeML and AGI safety? — Ramana Kumar (10 min)
Lunch
13:30 - 15:00
- adding priority queues to the basis — Quentin Ladeveze (25 min)
- what's new in FloVer and Icing — Heiko Becker (15 min)
- signatures and source semantics — Scott Owens (10 min)
- up-coming infix syntax and other syntax — Michael Norrish (10 min)
- discussion: documentation and infrastructure (30 min)
- for the CakeML language and compiler — Magnus Myreen, Scott Owens
- for the CakeML proofs and regression tests — Alejandro Gomez
Break
15:20 - 16:40
- working on CakeML in Coq — TJ Barclay joins via video link (10 min)
- clean up of monadic translator — Hrutvik Kanabar (15 min)
- what next for Isabelle/HOL CakeML translator? — Jonas Raedle and Lars Hupel (15 min)
- proving correctness of diverging programs — Magnus Myreen (10 min)
- discussion: making CakeML more usable (30 min)
- building on CakeML in other proof assistants
- future direction for the translator and CF
Social event and dinner starting 17:15
- a few rounds of boule at the Boulebar followed by dinner there
- we will walk from Chalmers to Boulebar together, starting from Chalmers at 16:40
Day 2 — Tuesday 14 May 2019 — "Hacking day"
09:15
- Coffee/tea outside meeting room
09:30 - 10:30
- discussion: drawing up a roadmap for the future of CakeML (60 min)
Break
10:50 - 12:00
- hash tables and buffered I/O — John Lind and Nebojsa Mihajlovic (20 min)
- proving lack of out-of-memory errors — Alejandro Gomez and Magnus Myreen (15 min)
- CakeML not a perfect fit for VeriPhy — Yong Kiam Tan (15 min)
- Pancake: a new thin source language — Magnus Myreen (15 min)
Lunch
13:30 - 15:00
- general hacking (90 min)
Break
15:20 - 17:00
- general hacking and/or revisiting the roadmap from the first session
Contact
Contact Magnus Myreen for more information or to request changes to the programme.