CakeML Developers Meeting 2018

A discussion about the future development and use of CakeML

Date:  29 May 2018
Venue:  D&IT room 8103, Chalmers, Sweden

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). 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.

Format

There is a programme with presentations (see below). The idea is that each presentation leaves a lot of 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. White boards can be used but are not particularly convenient in the meeting room.

Programme

This programme was put together to start with applications of CakeML and recent uses of CakeML, and then gradually move towards familiar core CakeML development (e.g. compiler hacking). The idea is that the recent uses of CakeML might influence the planning of future core development.

09:15

• Coffee/tea at the lunchroom before the meeting starts

09:30 - 10:30

• general introduction (15 min)
• everyone introduces themselves (15 min)
• the CASE project at Data61 — Johannes Åman Pohjola (30 min)

Break

10:50 - 12:00

• choreographies — Alejandro Gomez and Johannes Åman Pohjola (30 min)
• CakeML code gen. in Isabelle/HOL & AFP news — Lars Hupel (20 min)
• hardware — Andreas Lööw (20 min)

Lunch

13:30 - 15:00

• FloVer and FastMath — Heiko Becker (20 min)
• Candle: basis and article checker — Freek Wiedijk, Oskar Abrahamsson (30 min)
• use of CakeML in VeriPhy project at CMU — Yong Kiam Tan via Hangouts (20 min)
• discussion: How can we facilitate building on top of CakeML? What applications should be encouraged?

Break

15:20 - 16:40

• the new clos_known — Alexander Mihajlovic (20 min)
• linear scan register allocation — Théophile Wallez (15 min)
• common-subexpression elimination — Magnus presenting Nicholas Coughlin's work (10 min)
• a simple language — Magnus Myreen (10 min)
• discussion: How to manage the large code base? In which direction should CakeML develop?

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

Contact

Contact Magnus Myreen for more information or to request changes to the programme.