CoPLaWS is a series of annual workshops for programming language researchers working in the greater Copenhagen area, open to academics (DTU, KU, ITU, RUC, AAU CPH) and researchers in industry and other institutions. The aim is to get together and learn about each other’s work.
CoPLaWS 2024 is the second edition of the workshop. It will take place on Friday 23 August 2024 at the DTU Meeting Centre in Lyngby, room M1. It will be a full-day event including dinner (at the expense of the participants).
Title: Embedding Languages in Lean
Abstract: Lean is both an interactive theorem prover and a functional programming language. The Lean compiler, which is written in Lean itself, has an extensible frontend, including a customizable parser, a Racket-inspired hygienic macro system, and a rich compiler API that is used to implement both Lean’s tactic framework and its own elaborator. These features make Lean into a capable host for embedded domain-specific languages. This talk will be an example-driven tour of what is made possible for EDSLs by the coming together of the traditions of typed functional programming, Racket, and interactive theorem provers based on dependent types in Lean.
| 08:40 | Coffee & croissants |
| 08:55 | Welcome to CoPLaWS 2024 |
| 09:00 | Invited talk: David Thrane Christiansen. Embedding Languages in Lean. |
| 09:50 | Fritz Henglein and Changjun Li. Experimental evaluation of algebraic joins: Preliminary results. |
| 10:10 | Rodrigo Laigner and Yongluan Zhou. A progress report on AsyncDB: A native database system for asynchronous programs. |
| 10:30 | Coffee break |
| 10:50 | Oliver Bøving and Christoph Matheja. The weakest pre-expectation is equals to the expected reward. |
| 11:10 | Einar Broch Johnsen, Eduard Kamburjan, Raúl Pardo, Erik Voogd, and Andrzej Wąsowski. Towards a Proof System for Probabilistic Dynamic Logic. |
| 11:30 | Dawit Tirore, Jesper Bengtson and Marco Carbone. Multiparty Asynchronous Session Types: A Mechanised proof of Subject Reduction. |
| 11:50 | Radosław Rowicki, Adrian Francalanza and Alceste Scalas. Formalising and Verifying Monitors for Decentralised Deadlock Detection. |
| 12:10 | Lunch at the canteen in DTU Building 202 |
| 13:40 | Florian Furbach, Roland Kuhn, Alceste Scalas and Emilio Tuosto. Compositional Verification of Swarm Protocols. |
| 14:00 | Philipp Haller, Ayman Hussein, Hernan Melgratti, Alceste Scalas and Emilio Tuosto. Fair Join Pattern Matching for Actors. |
| 14:20 | Emil Kristensen, Marco Carbone and Alessandro Bruni. Gradual Session Typing in Erlang. |
| 14:40 | Coffee & cake break |
| 15:00 | John P. Gallagher. Transforming big-step to small-step semantics by specialisation of a Horn clause interpreter. |
| 15:20 | Maaike Zwart. Monads as (non)-compositional structures. |
| 15:40 | Joachim Tilsted Kristensen, Robin Kaarsgaard and Michael Kirkedal Thomsen. Jeopardy: An Invertible Functional Programming Language. |
| 16:00 | Hans Hüttel and Nicky Ask Lund. A type system for data flow and alias analysis in ReScript. |
| 16:20 | Break |
| 16:40 | Thomas Hildebrandt. Object-Centric Declarative Programming with DCR Graphs. |
| 17:00 | Christian Kalhauge. Input Reduction with Reduction Trees. |
| 17:20 | Maja Hanne Kirkeby, Michael Kirkedal Thomsen and Ken Friis Larsen. 10 years of GCC from an energy perspective. |
| 17:40 | End of scientific programme |
| 19:00 | Dinner at Meyers Spisehus in Lyngby |
Alceste Scalas, Fritz Henglein, Hugo-Andres Lopez-Acosta, Marco Carbone, Morten Rhiger, Rasmus Møgelberg.
CoPLaWS 2024 is sponsored by DTU Compute - Section for Software Systems Engineering.