diff --git a/data/planet/watch-ocaml/casually-talking-about-rescript-oss-and-communities-with-patrick-ecker.md b/data/planet/watch-ocaml/casually-talking-about-rescript-oss-and-communities-with-patrick-ecker.md deleted file mode 100644 index ab2fa765a6..0000000000 --- a/data/planet/watch-ocaml/casually-talking-about-rescript-oss-and-communities-with-patrick-ecker.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Casually talking about ReScript, OSS, and communities with Patrick Ecker -description: Patrick (@ryyppy) is working with OSS in ReScript and part of the core - team If you'd like to support the show for more content about OCaml, Reason and - ReScript you can now do so at https://www.pat... -url: https://watch.ocaml.org/w/diKYNSqbUGEsDZ6hXxDvck -date: 2023-03-17T19:00:54-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/848210e7-82e6-45f0-b968-e350d8e0d29a.jpg -authors: -- Watch OCaml -source: ---- - -

Patrick (@ryyppy) is working with OSS in ReScript and part of the core team

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/casually-talking-with-craig-ferguson-about-ocaml-mirage-irmin-and-more.md b/data/planet/watch-ocaml/casually-talking-with-craig-ferguson-about-ocaml-mirage-irmin-and-more.md deleted file mode 100644 index 66a1dd38a6..0000000000 --- a/data/planet/watch-ocaml/casually-talking-with-craig-ferguson-about-ocaml-mirage-irmin-and-more.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: Casually talking with Craig Ferguson about OCaml, Mirage, Irmin and more -description: Craig Ferguson is a software developer at Tarides. Join us in this episode - to talk more about OCaml, MirageOS, Irmin and much more! We are looking for sponsors! - If you'd like to support more conten... -url: https://watch.ocaml.org/w/w6aaXz285friXnPE6p2eqP -date: 2023-03-17T20:58:09-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/46045ddd-f525-4230-95e7-a63d7682fe3c.jpg -authors: -- Watch OCaml -source: ---- - -

Craig Ferguson is a software developer at Tarides. Join us in this episode to talk more about OCaml, MirageOS, Irmin and much more!

-

We are looking for sponsors! If you'd like to support more content for Ocaml, Reason and ReScript just send us a message at emelletvshow@gmail.com -- Watch live at https://www.twitch.tv/emelletv

-

0:00 Welcome
-1:57 Interview starts

- diff --git a/data/planet/watch-ocaml/casually-talking-with-eduardo-rafael-about-ocaml-tezos-and-probably-compilers.md b/data/planet/watch-ocaml/casually-talking-with-eduardo-rafael-about-ocaml-tezos-and-probably-compilers.md deleted file mode 100644 index a07a2f8f48..0000000000 --- a/data/planet/watch-ocaml/casually-talking-with-eduardo-rafael-about-ocaml-tezos-and-probably-compilers.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: Casually talking with Eduardo Rafael about OCaml, Tezos and probably compilers -description: Eduardo is a streamer and a tech lead at @Marigold_Dev. Join us in this - episode to casually talk about OCaml, Tezos and probably compilers If you'd like - to support the show for more content about O... -url: https://watch.ocaml.org/w/3bxFjLNQ5JwHdAvXcHHdG1 -date: 2023-03-17T20:08:38-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/335293ad-9f20-4271-b792-652e97b88be2.jpg -authors: -- Watch OCaml -source: ---- - -

Eduardo is a streamer and a tech lead at @Marigold_Dev.
-Join us in this episode to casually talk about OCaml, Tezos and probably compilers

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/casually-talking-with-gabriel-radanne-about-ocaml-meta-programming-and-much-more.md b/data/planet/watch-ocaml/casually-talking-with-gabriel-radanne-about-ocaml-meta-programming-and-much-more.md deleted file mode 100644 index 3863bf05b9..0000000000 --- a/data/planet/watch-ocaml/casually-talking-with-gabriel-radanne-about-ocaml-meta-programming-and-much-more.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: Casually talking with Gabriel Radanne about OCaml, meta-programming and much - more -description: Gabriel "Drup" Radanne researcher at Inria in the CASH research team - If you'd like to support the show for more content about OCaml, Reason and ReScript you - can now do so at https://www.patreon.co... -url: https://watch.ocaml.org/w/fdA2RG8tFbNojSFUYJRcv7 -date: 2023-03-17T20:37:42-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/a61f1dcc-41ae-4785-9212-c81b861c3565.jpg -authors: -- Watch OCaml -source: ---- - -

Gabriel "Drup" Radanne researcher at Inria in the CASH research team

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/casually-talking-with-hongbo-zhang.md b/data/planet/watch-ocaml/casually-talking-with-hongbo-zhang.md deleted file mode 100644 index 8a86131e24..0000000000 --- a/data/planet/watch-ocaml/casually-talking-with-hongbo-zhang.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Casually talking with Hongbo Zhang -description: Hongbo Zhang (@bobzhang1988), creator of BuckleScript and core maintainer - of ReScript Enjoying the video? Please, support the show for more content about - OCaml, Reason and ReScript you can now do s... -url: https://watch.ocaml.org/w/6RR6AjEY5FJLmb1iUohcvu -date: 2023-03-17T19:57:51-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/958bfa54-0e85-4a70-9bf7-ba3fab4d42bd.jpg -authors: -- Watch OCaml -source: ---- - -

Hongbo Zhang (@bobzhang1988), creator of BuckleScript and core maintainer of ReScript

-

Enjoying the video? Please, support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/causally-talking-with-sean-grove-about-graphql-onegraph-and-reasonml.md b/data/planet/watch-ocaml/causally-talking-with-sean-grove-about-graphql-onegraph-and-reasonml.md deleted file mode 100644 index 3208b38eab..0000000000 --- a/data/planet/watch-ocaml/causally-talking-with-sean-grove-about-graphql-onegraph-and-reasonml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Causally talking with Sean Grove about GraphQL, OneGraph and ReasonML -description: Sean Grove Founder of OneGraph If you'd like to support the show for - more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv - or by sending any tez amoun... -url: https://watch.ocaml.org/w/wEiEDtiRWuqddnFopZKDi5 -date: 2023-03-17T20:21:19-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/50ece6ab-187f-4849-9bb2-9ec1fa56cabd.jpg -authors: -- Watch OCaml -source: ---- - -

Sean Grove Founder of OneGraph

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/debugging-native-ocaml-with-breakpoints-and-stepping.md b/data/planet/watch-ocaml/debugging-native-ocaml-with-breakpoints-and-stepping.md deleted file mode 100644 index a31728e59d..0000000000 --- a/data/planet/watch-ocaml/debugging-native-ocaml-with-breakpoints-and-stepping.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -title: Debugging Native OCaml with Breakpoints and Stepping -description: -url: https://watch.ocaml.org/w/c6jKXFzwgrFzSwnxTM6eGX -date: 2023-07-07T17:18:45-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/dc13adc1-5f71-4ef0-8c59-203f9bec8215.jpg -authors: -- Watch OCaml -source: ---- - - diff --git a/data/planet/watch-ocaml/demo-solo5-unikernel-hosting-the-mirageos-www-htdocs-on-a-raspberry-pi.md b/data/planet/watch-ocaml/demo-solo5-unikernel-hosting-the-mirageos-www-htdocs-on-a-raspberry-pi.md deleted file mode 100644 index 6447639fd2..0000000000 --- a/data/planet/watch-ocaml/demo-solo5-unikernel-hosting-the-mirageos-www-htdocs-on-a-raspberry-pi.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -title: 'Demo: Solo5 Unikernel Hosting the MirageOS www-htdocs on a Raspberry Pi' -description: A demo showing a Solo5 unikernel hosting the MirageOS www-htdocs on a - Raspberry Pi -url: https://watch.ocaml.org/w/1RhQXW5NNqRtdxXgi12pD9 -date: 2023-09-20T11:27:06-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/93a0d1d1-f3f7-4e4f-aaa8-a54aa77cbabc.jpg -authors: -- Watch OCaml -source: ---- - -

A demo showing a Solo5 unikernel hosting the MirageOS www-htdocs on a Raspberry Pi

- diff --git a/data/planet/watch-ocaml/develop-cross-platform-software-using-2-languages.md b/data/planet/watch-ocaml/develop-cross-platform-software-using-2-languages.md deleted file mode 100644 index 1cf012effe..0000000000 --- a/data/planet/watch-ocaml/develop-cross-platform-software-using-2-languages.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: Develop Cross-Platform Software using 2+ Languages -description: 'Explore how high school robotics software was developed that works on - Android phones and desktop PCs. Use OCaml alongside common programming languages - like Java and Python. DkSDK Subscription: http...' -url: https://watch.ocaml.org/w/d2uoLa5wHcjQ4az4BNNtZA -date: 2023-11-16T22:18:27-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/d0b92b8c-bfa0-4de0-aa07-1ee9f09957b1.jpg -authors: -- Watch OCaml -source: ---- - -

Explore how high school robotics software was developed that works on Android phones and desktop PCs. Use OCaml alongside common programming languages like Java and Python.

-

DkSDK Subscription: https://diskuv.com/pricing/
-Learning OCaml: https://ocaml.org/docs
-First Robotics: https://www.firstinspires.org/robotics/frc

- diff --git a/data/planet/watch-ocaml/episode3-youtube.md b/data/planet/watch-ocaml/episode3-youtube.md deleted file mode 100644 index a20f8e8358..0000000000 --- a/data/planet/watch-ocaml/episode3-youtube.md +++ /dev/null @@ -1,26 +0,0 @@ ---- -title: Episode3-Youtube -description: Everything you need to know to install and use the DkML distribution - of OCaml on Windows. Includes a 5-minute quick install for learners. Includes how - to setup projects and configuring IDEs for sof... -url: https://watch.ocaml.org/w/awwFLmzJMvQfHzTkTARMdn -date: 2023-12-08T12:14:13-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/a8a8b99d-ed5a-4526-81a1-9cff0aad49b1.jpg -authors: -- Watch OCaml -source: ---- - -

Everything you need to know to install and use the DkML distribution of OCaml on Windows. Includes a 5-minute quick install for learners. Includes how to setup projects and configuring IDEs for software creators/engineers.

-

At the time of this video publication, the ocaml.org website had not been updated to include the instructions in this video. However, the video is self-contained.

-

Helpful callouts from the video:

-

1- Using PowerShell to create initial files for a new project:

-

New-Item dune-project -Value "(lang dune 3.12)"
-New-Item dune -Value "(executable (name main))"
-New-Item main.ml -Value "let = print_endline {|Hello! Press ENTER to quit.|} ; input_char stdin"

-

2- The .ocamlformat to enable formatting of your source code:

-

version=0.25.1
-profile=conventional
-exp-grouping=preserve
-nested-match=align

- diff --git a/data/planet/watch-ocaml/ocaml-behind-the-scenes-exceptions.md b/data/planet/watch-ocaml/ocaml-behind-the-scenes-exceptions.md deleted file mode 100644 index 82541eec67..0000000000 --- a/data/planet/watch-ocaml/ocaml-behind-the-scenes-exceptions.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: 'OCaml behind the scenes: Exceptions' -description: In this talk, Fabrice Buoro explained what happens at the deepest level - when your OCaml program raises or catches an exception. This inside knowledge will - lead to a number of takeaways for best per... -url: https://watch.ocaml.org/w/vur2uhCFTZWQfDfkcbCPfC -date: 2023-07-27T16:00:17-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/4b2dd6ed-9290-4b99-80ef-af1f76213568.jpg -authors: -- Watch OCaml -source: ---- - -

In this talk, Fabrice Buoro explained what happens at the deepest level when your OCaml program raises or catches an exception. This inside knowledge will lead to a number of takeaways for best performance.

-

Slides and sources can be found at https://github.com/fabbing/obts_exn.

- diff --git a/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md b/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md deleted file mode 100644 index 10b228bed7..0000000000 --- a/data/planet/watch-ocaml/ocaml23-buck2-for-ocaml-users--developers.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Buck2 for OCaml Users & Developers' -description: '[OCaML''23] Buck2 for OCaml Users & Developers Shayne Fletcher, Neil - Mitchell Buck2 is an open-source large scale build system used by thousands of developers - at Meta every day. Buck2 can be use...' -url: https://watch.ocaml.org/w/cYiKFa5EbS3AqVgYzMHP5V -date: 2024-09-29T15:48:58-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/2b327168-249c-466f-a99b-bc1bde243dc7.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Buck2 for OCaml Users & Developers

-

Shayne Fletcher, Neil Mitchell

-

Buck2 is an open-source large scale build system used by thousands of developers at Meta every day. Buck2 can be used to build OCaml with some useful advantages over alternatives (e.g. Dune or Bazel). In this talk we’ll discuss what those advantages are, why they arise, and how to use Buck2 for your OCaml development.

- diff --git a/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md b/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md deleted file mode 100644 index bfb26f989c..0000000000 --- a/data/planet/watch-ocaml/ocaml23-building-a-lock-free-stm-for-ocaml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Building a lock-free STM for OCaml' -description: '[OCaML''23] Building a lock-free STM for OCaml Vesa Karvonen, Bartosz - Modelski, Carine Morel, Thomas Leonard, KC Sivaramakrishnan, YSS Narasimha Naidu, - Sudha Parimala The kcas library was originally...' -url: https://watch.ocaml.org/w/v3LtkXGeW5KXjziPQdzRJZ -date: 2024-09-29T15:39:28-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/38e8d543-9ec5-4354-9e04-985d09d22571.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Building a lock-free STM for OCaml

-

Vesa Karvonen, Bartosz Modelski, Carine Morel, Thomas Leonard, KC Sivaramakrishnan, YSS Narasimha Naidu, Sudha Parimala

-

The kcas library was originally developed to provide a primitive atomic lock-free multi-word compare-and-set operation. This talk introduces kcas and discusses the recent development of kcas turning it into a proper lock-free software transactional memory implementation for OCaml that provides composable transactions, scheduler friendly modular blocking, and comes with a companion library of composable lock-free data structures.

- diff --git a/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md b/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md deleted file mode 100644 index 3487bf1160..0000000000 --- a/data/planet/watch-ocaml/ocaml23-efficient-ocaml-compilation-with-flambda-2.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Efficient OCaml compilation with Flambda 2' -description: '[OCaML''23] Efficient OCaml compilation with Flambda 2 Pierre Chambart, - Vincent LAVIRON, Mark Shinwell Flambda 2 is an IR and optimisation pass for OCaml - centred around inlining. We discuss the engi...' -url: https://watch.ocaml.org/w/qGN45zFDCVGxiKRz9mKkVp -date: 2024-09-29T16:01:22-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/54d5501a-b6ae-4106-bbdc-dbd09ab7da33.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Efficient OCaml compilation with Flambda 2

-

Pierre Chambart, Vincent LAVIRON, Mark Shinwell

-

Flambda 2 is an IR and optimisation pass for OCaml centred around inlining. We discuss the engineering constraints that shaped it and the overall structure that allows the compiler to be fast enough to handle very large industrial code bases.

- diff --git a/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md b/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md deleted file mode 100644 index 7a8fd7d36c..0000000000 --- a/data/planet/watch-ocaml/ocaml23-eio-10--effects-based-io-for-ocaml-5.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5" -description: "[OCaML'23] Eio 1.0 \u2013 Effects-based IO for OCaml 5 Thomas Leonard, - Patrick Ferris, Christiano Haesbaert, Lucas Pluvinage, Vesa Karvonen, Sudha Parimala, - KC Sivaramakrishnan, Vincent Balat, Anil Madh..." -url: https://watch.ocaml.org/w/9Hxc81ac3k6GQF1fdZLx7d -date: 2024-09-29T16:13:37-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/66c29989-c956-45aa-b582-84a311c086fc.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Eio 1.0 – Effects-based IO for OCaml 5

-

Thomas Leonard, Patrick Ferris, Christiano Haesbaert, Lucas Pluvinage, Vesa Karvonen, Sudha Parimala, KC Sivaramakrishnan, Vincent Balat, Anil Madhavapeddy

-

Eio provides an effects-based direct-style IO stack for OCaml 5. This talk introduces Eio’s main features, such as use of effects, multi-core support and lock-free data-structures, support for modular programming, interoperability with other concurrency libraries such as Lwt, Async and Domainslib, and interactive monitoring support enabled by the custom runtime events in OCaml 5.1. We will report on our experiences porting existing applications to Eio.

- diff --git a/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md b/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md deleted file mode 100644 index 1c07c3e1cd..0000000000 --- a/data/planet/watch-ocaml/ocaml23-less-power-for-more-learning-restricting-ocaml-features-for-effective-teaching.md +++ /dev/null @@ -1,19 +0,0 @@ ---- -title: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features for Effective - Teaching' -description: '[OCaML''23] Less Power for More Learning: Restricting OCaml Features - for Effective Teaching Max Lang, Nico Petzendorfer We present a framework for sandboxing - and restricting features of the OCaml pr...' -url: https://watch.ocaml.org/w/uABzLbyAasoKbjyRwganh4 -date: 2024-09-29T16:04:22-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/9915ec4a-8c53-46e5-b06d-61e1c91940b9.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Less Power for More Learning: Restricting OCaml Features for Effective Teaching

-

Max Lang, Nico Petzendorfer

-

We present a framework for sandboxing and restricting features of the OCaml programming language to effectively automate the grading of programming exercises, scaling to hundreds of submissions. We describe how to disable language and library features that should not be used to solve a given exercise. We present an overview of an implementation of a mock IO system to allow testing of IO-related exercises in a controlled environment. Finally, we detail a number of security considerations to ensure submitted code remains sandboxed, allowing automatic grading to be trusted without manual verification. The source code of our implementation is publicly available [1].
-[1] As a git repository at https://github.com/just-max/less-power.

- diff --git a/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md b/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md deleted file mode 100644 index 46ebbdcfc4..0000000000 --- a/data/planet/watch-ocaml/ocaml23-metaocaml-theory-and-implementation.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] MetaOCaml Theory and Implementation' -description: '[OCaML''23] MetaOCaml Theory and Implementation Oleg Kiselyov Quasi-quotation - (or, code templates) has long been used as a convenient tool for code generation, - commonly implemented as a pre-processi...' -url: https://watch.ocaml.org/w/rnQXcND8aaY9qUtikB9tSc -date: 2024-09-29T15:35:39-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/6fb93c0e-5afe-4a67-a158-00f303af7e44.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] MetaOCaml Theory and Implementation

-

Oleg Kiselyov

-

Quasi-quotation (or, code templates) has long been used as a convenient tool for code generation, commonly implemented as a pre-processing/translation into code-generation combinators. The original MetaOCaml was also based on such translation, done post type checking. BER MetaOCaml employs a significantly different, efficient (especially in version N114) translation integrated with type-checking, in the least intrusive way. This paper presents the integrated efficient translation for the first time.

- diff --git a/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md b/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md deleted file mode 100644 index 613fc94c47..0000000000 --- a/data/planet/watch-ocaml/ocaml23-modern-dsl-compiler-architecture-in-ocaml-our-experience-with-catala.md +++ /dev/null @@ -1,20 +0,0 @@ ---- -title: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience with - Catala' -description: '[OCaML''23] Modern DSL compiler architecture in OCaml our experience - with Catala Louis Gesbert, Denis Merigoux In this presentation, we intend to show - a state-of-the-art DSL implementation in OCaml,...' -url: https://watch.ocaml.org/w/7ZxKnBY2w3XCztpzbKm8YG -date: 2024-09-29T16:16:23-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/7584602b-9668-4289-bb86-e9721e157f8b.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Modern DSL compiler architecture in OCaml our experience with Catala

-

Louis Gesbert, Denis Merigoux

-

In this presentation, we intend to show a state-of-the-art DSL implementation in OCaml, with concrete examples and experience reports.
-In particular, we found that some advanced practices, while accepted among the hardcore OCaml developers (e.g. use of row type variables through object types), lacked visibility and documentation: some of them deserve to be better known.
-Our experience is based on the Catala compiler, a DSL for the implementation of algorithms defined in law.

- diff --git a/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md b/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md deleted file mode 100644 index e93087ec8a..0000000000 --- a/data/planet/watch-ocaml/ocaml23-osiris-an-iris-based-program-logic-for-ocaml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Osiris: an Iris-based program logic for OCaml' -description: "[OCaML'23] Osiris: an Iris-based program logic for OCaml Arnaud Daby-Seesaram, - Fran\xE7ois Pottier, Arma\xEBl Gu\xE9neau Osiris is a project that aims to help - OCaml developers verify their code using Separa..." -url: https://watch.ocaml.org/w/1Hfi9pjTo1hz1ej2WtVGCR -date: 2024-09-29T15:27:45-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/01208c4e-6774-4946-9ff6-69e0375dc3c2.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Osiris: an Iris-based program logic for OCaml

-

Arnaud Daby-Seesaram, François Pottier, Armaël Guéneau

-

Osiris is a project that aims to help OCaml developers verify their code using Separation Logic. The project is still young: we currently only support a subset of the features of the OCaml language, including modules, mutual recursion, ADTs, tuples and records. Ultimately, we would like to extend Osiris to support most features of the OCaml language. Iris is a Coq framework for Separation Logic with support for expressive ghost states. It is often used to define program logics and can be parameterized by a programming language — usually described by its small-steps semantics. Most Iris instantiations target ML-like languages, each focusing on a specific purpose and lacking support of programming features such as records or ADTs. Osiris contains an Iris instantiation with a presentation of the semantics of OCaml, in order to reason on realistic OCaml programs. Osiris provides a translation tool to convert OCaml files to Coq files (cf. section 2). In order to verify an OCaml program with Osiris, one would use the translator on an OCaml file, seen as a module. This produces a Coq file containing a deep-embedded representation me of the module. The user would then write and prove a specification for the interpretation of me in our semantics.

- diff --git a/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md b/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md deleted file mode 100644 index 23b3d6654f..0000000000 --- a/data/planet/watch-ocaml/ocaml23-owi-an-interpreter-and-a-toolkit-for-webassembly-written-in-ocaml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Owi: an interpreter and a toolkit for WebAssembly written in OCaml' -description: "[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written - in OCaml L\xE9o Andr\xE8s, Pierre Chambart, Eric Patrizio, Dario Pinto This presentation - introduces Owi, an OCaml-based interpreter an..." -url: https://watch.ocaml.org/w/3pYGmveWpNNLH4B6TUv5ww -date: 2024-09-29T15:25:04-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/da695cb1-3459-48bc-949b-ab4b84263c1e.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Owi: an interpreter and a toolkit for WebAssembly written in OCaml

-

Léo Andrès, Pierre Chambart, Eric Patrizio, Dario Pinto

-

This presentation introduces Owi, an OCaml-based interpreter and toolkit for WebAssembly (Wasm). Owi aims to provide a fast and easily maintainable solution for Wasm code execution. Unlike competing interpreters, Owi focuses on facilitating experimentation, research, and symbolic manipulations of Wasm. We describe the different passes and intermediate representations of Owi. Additionally, we discuss the linker, the interpreter and its support for various Wasm-specific extensions. Owi’s API leverages Generalized Algebraic Data Types (GADTs) for improved error detection at link-time. We also describe the testing methods used, including a Crowbar-based fuzzer. Future work includes incorporating missing Wasm extensions, implementing advanced optimization passes, and potentially porting the WASP execution engine to perform concolic execution.

- diff --git a/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md b/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md deleted file mode 100644 index 6508c913bc..0000000000 --- a/data/planet/watch-ocaml/ocaml23-parallel-sequences-in-multicore-ocaml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: '[OCaML''23] Parallel Sequences in Multicore OCaml' -description: '[OCaML''23] Parallel Sequences in Multicore OCaml Andrew Tao I present - my implementation of a parallel sequences abstraction that utilizes the support - for shared memory parallelism in the new OCaml ...' -url: https://watch.ocaml.org/w/6K7mqY88PyDZFC2bJvs2Xe -date: 2024-09-29T15:40:29-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/fe7678aa-6348-45bd-b293-caf5f8877e35.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Parallel Sequences in Multicore OCaml

-

Andrew Tao

-

I present my implementation of a parallel sequences abstraction that utilizes the support for shared memory parallelism in the new OCaml 5.0.0 multicore runtime. This abstraction allows clients to create highly parallelizable programs without needing to write, or even understand, the low-level implementation details necessary to parallelize large tasks.

- diff --git a/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md b/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md deleted file mode 100644 index 8e9f6ab1e6..0000000000 --- a/data/planet/watch-ocaml/ocaml23-state-of-the-ocaml-platform-2023.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -title: '[OCaML''23] State of the OCaml Platform 2023' -description: '[OCaML''23] State of the OCaml Platform 2023 Thibaut Mattio, Anil Madhavapeddy, - Thomas Gazagnaire, David Allsopp This paper reflects on a decade of progress and - developments within the OCaml Platfor...' -url: https://watch.ocaml.org/w/9GtFUSDDpmU8ZDD54A7V7e -date: 2024-09-29T15:27:19-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/96763544-5622-470d-8ef0-bdd191d657e7.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] State of the OCaml Platform 2023

-

Thibaut Mattio, Anil Madhavapeddy, Thomas Gazagnaire, David Allsopp

-

This paper reflects on a decade of progress and developments within the OCaml Platform, from its inception in 2013 with the release of opam 1.0, to today where it stands as a robust toolchain for OCaml developers. We review the last three years in detail, emphasizing the advancements and innovations that have shaped the OCaml development landscape and highlighting key milestones such as the migration to Dune as the primary build system, and the development of a Language Server Protocol (LSP) server for OCaml.
-We also outline our plan for the coming years. The roadmap is informed by community feedback, discussions with Platform tool maintainers, and insights from industrial users of OCaml. The final version of this evolving roadmap, designed to shape the future of the OCaml developer experience, will be presented at the International Conference on Functional Programming (ICFP).

- diff --git a/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md b/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md deleted file mode 100644 index df83d7a712..0000000000 --- a/data/planet/watch-ocaml/ocaml23-targeted-static-analysis-for-ocaml-c-stubs-eliminating-gremlins-from-the-code.md +++ /dev/null @@ -1,20 +0,0 @@ ---- -title: '[OCaML''23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins - from the code' -description: "[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins - from the code Edwin T\xF6r\xF6k Migration to OCaml 5 requires updating a lot of - C bindings due to the removal of naked pointer ..." -url: https://watch.ocaml.org/w/sj5jf9iieZA7E1cbDbnv2j -date: 2024-09-29T14:32:44-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/02fc8f1e-7e60-4f76-af5f-8228533fb06f.jpg -authors: -- Watch OCaml -source: ---- - -

[OCaML'23] Targeted Static Analysis for OCaml C Stubs: Eliminating gremlins from the code

-

Edwin Török

-

Migration to OCaml 5 requires updating a lot of C bindings due to the removal of naked pointer support. Writing OCaml user-defined primitives in C is a necessity, but is unsafe and error-prone. It does not benefit from either OCaml’s or C’s type checking, and existing C static analysers are not aware of the OCaml GC safety rules, and cannot infer them from existing macros alone. The alternative is automatically generating C stubs, which requires correctly managing value lifetimes. Having a static analyser for OCaml to C interfaces is useful outside the OCaml 5 porting effort too.
-After some motivating examples of real bugs in C bindings a static analyser is presented that finds these known classes of bugs. The tool works on the OCaml abstract parse and typed trees, and generates a header file and a caller model. Together with a simplified model of the OCaml runtime this is used as input to a static analysis framework, Goblint. An analysis is developed that tracks dereferences of OCaml values, and together with the existing framework reports incorrect dereferences. An example is shown how to extend the analysis to cover more safety properties.
-The tools and runtime models are generic and could be reused with other static analysis tools.

- diff --git a/data/planet/watch-ocaml/ocsigen-developing-web-and-mobile-applications-in-ocaml--jrme-vouillon--vincent-balat.md b/data/planet/watch-ocaml/ocsigen-developing-web-and-mobile-applications-in-ocaml--jrme-vouillon--vincent-balat.md deleted file mode 100644 index f233ab0060..0000000000 --- a/data/planet/watch-ocaml/ocsigen-developing-web-and-mobile-applications-in-ocaml--jrme-vouillon--vincent-balat.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: "Ocsigen: Developing Web and mobile applications in OCaml \u2013 J\xE9r\xF4me - Vouillon & Vincent Balat" -description: This presentation gives an overview of the Ocsigen framework, which is - used in particular to develop the Be Sport social network. Ocsigen is a set a tools - to develop Web sites and applications. Amo... -url: https://watch.ocaml.org/w/qQzb94X9WM7zLif7FynPyN -date: 2024-01-23T10:29:15-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/1ffd7d0d-7e38-4d59-b936-44a6ebd00041.jpg -authors: -- Watch OCaml -source: ---- - -

This presentation gives an overview of the Ocsigen framework, which is used in particular to develop the Be Sport social network. Ocsigen is a set a tools to develop Web sites and applications. Amongst other things, it contains js_of_ocaml, a compiler to Javascript, and Eliom, a powerful Web framework that can be used for traditional server-side Web programming, but also to develop client-server Web and mobile distributed applications, fully in OCaml, using multi-tier programming. This programming style can save a huge amount of time.

- diff --git a/data/planet/watch-ocaml/outreachy-may-2024-demo.md b/data/planet/watch-ocaml/outreachy-may-2024-demo.md deleted file mode 100644 index 7aa6d3f787..0000000000 --- a/data/planet/watch-ocaml/outreachy-may-2024-demo.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: Outreachy May 2024 Demo -description: The OCaml community participated in the May 2024 round of Outreachy internships. - Three interns worked on a range of projects including tools to diff OCaml APIs, - more accessible diffing tools and ru... -url: https://watch.ocaml.org/w/peT3MdWjS1BYYMbowEJ1gv -date: 2024-09-07T15:07:21-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/1a1f5808-073c-4970-86cb-f60729386693.jpg -authors: -- Watch OCaml -source: ---- - -

The OCaml community participated in the May 2024 round of Outreachy internships. Three interns worked on a range of projects including tools to diff OCaml APIs, more accessible diffing tools and running OCaml exercises anywhere!

-

This meeting was an opportunity for the interns to present their work and for the community to ask questions and was originally announced on the discuss forum.

- diff --git a/data/planet/watch-ocaml/outreachy-presentations-for-the-december-2023-round.md b/data/planet/watch-ocaml/outreachy-presentations-for-the-december-2023-round.md deleted file mode 100644 index d633b6608c..0000000000 --- a/data/planet/watch-ocaml/outreachy-presentations-for-the-december-2023-round.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: Outreachy Presentations for the December 2023 Round -description: The OCaml community participated in the December 2023 round of Outreachy - internships. Three interns worked on a range of projects including geometric creative - coding libraries, dark mode for OCaml.... -url: https://watch.ocaml.org/w/b7sv1LQSVZQH6trf4xpwFX -date: 2024-03-08T17:55:29-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/029558c7-40f6-4403-afd9-c10b7d0f6288.jpg -authors: -- Watch OCaml -source: ---- - -

The OCaml community participated in the December 2023 round of Outreachy internships. Three interns worked on a range of projects including geometric creative coding libraries, dark mode for OCaml.org and building GUIs in OCaml.

-

This meeting was an opportunity for the interns to present their work and for the community to ask questions and was originally announced on the discuss forum.

- diff --git a/data/planet/watch-ocaml/outreachy-presentations-for-the-may-2023-round.md b/data/planet/watch-ocaml/outreachy-presentations-for-the-may-2023-round.md deleted file mode 100644 index 17c6344cf6..0000000000 --- a/data/planet/watch-ocaml/outreachy-presentations-for-the-may-2023-round.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: Outreachy Presentations for the May 2023 Round -description: 'The OCaml community participated in the May 2023 round of Outreachy - internships. Three interns worked on a range of projects including: MIDI over ethernet, - persistent storage in MirageOS and improv...' -url: https://watch.ocaml.org/w/kTwq4AVQtRtFuQx9R5cPro -date: 2023-09-18T13:15:08-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/7fcd3128-d1c7-45e2-a420-aedb896a0189.jpg -authors: -- Watch OCaml -source: ---- - -

The OCaml community participated in the May 2023 round of Outreachy internships. Three interns worked on a range of projects including: MIDI over ethernet, persistent storage in MirageOS and improving error reporting in existing ppxlib-based ppxs.

-

This meeting was an opportunity for the interns to present their work and for the community to ask questions and was originally announced on the discuss forum.

- diff --git a/data/planet/watch-ocaml/talking-with-anil-madhavapeddy-about-ocaml-tezos-and-trustedcarbon.md b/data/planet/watch-ocaml/talking-with-anil-madhavapeddy-about-ocaml-tezos-and-trustedcarbon.md deleted file mode 100644 index 27d6d4ad61..0000000000 --- a/data/planet/watch-ocaml/talking-with-anil-madhavapeddy-about-ocaml-tezos-and-trustedcarbon.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Talking with Anil Madhavapeddy about OCaml, Tezos and @TrustedCarbon -description: Anil Madhavapeddy (@avsm), the face of OCaml If you'd like to support - the show for more content about OCaml, Reason and ReScript you can now do so at - https://www.patreon.com/emelletv or by sending... -url: https://watch.ocaml.org/w/iTDrQNvXnW5ENGbShXQVB6 -date: 2023-03-17T20:14:16-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/89fad1f6-7b6a-4713-be74-6d7cdd097352.jpg -authors: -- Watch OCaml -source: ---- - -

Anil Madhavapeddy (@avsm), the face of OCaml

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/talking-with-antnio-monteiro-about-melange--esy-reason-ocaml-and-more.md b/data/planet/watch-ocaml/talking-with-antnio-monteiro-about-melange--esy-reason-ocaml-and-more.md deleted file mode 100644 index b8e38a78d3..0000000000 --- a/data/planet/watch-ocaml/talking-with-antnio-monteiro-about-melange--esy-reason-ocaml-and-more.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -title: "Talking with Ant\xF3nio Monteiro about Melange, Esy, Reason, OCaml and more" -description: "If you would like to sponsor the show contact https://twitter.com/davesnx - Consider sponsoring Ant\xF3nio's work: https://github.com/sponsors/anmonteiro" -url: https://watch.ocaml.org/w/aEabwHEfXTKGxTNi6Xhy2a -date: 2023-03-17T21:10:48-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/426c0fbb-7368-4d30-ad78-7488fbd949fd.jpg -authors: -- Watch OCaml -source: ---- - -

If you would like to sponsor the show contact https://twitter.com/davesnx

-

Consider sponsoring António's work: https://github.com/sponsors/anmonteiro

- diff --git a/data/planet/watch-ocaml/talking-with-gabriel-nordeborn--rescript-relay-and-everything-else.md b/data/planet/watch-ocaml/talking-with-gabriel-nordeborn--rescript-relay-and-everything-else.md deleted file mode 100644 index c615da2aa4..0000000000 --- a/data/planet/watch-ocaml/talking-with-gabriel-nordeborn--rescript-relay-and-everything-else.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -title: Talking with Gabriel Nordeborn ReScript, Relay and everything else! -description: -url: https://watch.ocaml.org/w/u95Usnr46V4JCcdSdrBYim -date: 2023-03-17T21:20:37-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/49525c3c-8484-4347-b1d5-dea6f9f26899.jpg -authors: -- Watch OCaml -source: ---- - - diff --git a/data/planet/watch-ocaml/talking-with-jaap-frolich-about-graphql-ppx.md b/data/planet/watch-ocaml/talking-with-jaap-frolich-about-graphql-ppx.md deleted file mode 100644 index c3c3d03446..0000000000 --- a/data/planet/watch-ocaml/talking-with-jaap-frolich-about-graphql-ppx.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Talking with Jaap Frolich about graphql-ppx -description: Jaap (@JaapFrolich) is working at Walnut and maintainer of graphql-ppx - If you'd like to support the show for more content about OCaml, Reason and ReScript you - can now do so at https://www.patreon.... -url: https://watch.ocaml.org/w/frRb1XtP1JLqbkjVnEKZud -date: 2023-03-17T19:15:11-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/ef56fe77-5a54-4fce-89c3-b62c8c38618a.jpg -authors: -- Watch OCaml -source: ---- - -

Jaap (@JaapFrolich) is working at Walnut and maintainer of graphql-ppx

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/talking-with-oscar-spencer-about-grain-lang-wasm-plt-and-ml.md b/data/planet/watch-ocaml/talking-with-oscar-spencer-about-grain-lang-wasm-plt-and-ml.md deleted file mode 100644 index 58f5e25595..0000000000 --- a/data/planet/watch-ocaml/talking-with-oscar-spencer-about-grain-lang-wasm-plt-and-ml.md +++ /dev/null @@ -1,17 +0,0 @@ ---- -title: Talking with Oscar Spencer about Grain Lang, WASM, PLT and ML -description: Oscar Spencer @oscar_spen is the co-author of Grain Lang If you'd like - to support the show for more content about OCaml, Reason and ReScript you can now - do so at https://www.patreon.com/emelletv o... -url: https://watch.ocaml.org/w/q8Vk2EeT3THKmK9npmAn1e -date: 2023-03-17T19:33:34-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/42e04374-748c-4a47-ab35-f3ffaab9ee86.jpg -authors: -- Watch OCaml -source: ---- - -

Oscar Spencer @oscar_spen is the co-author of Grain Lang

-

If you'd like to support the show for more content about OCaml, Reason and ReScript you can now do so at https://www.patreon.com/emelletv or by sending any tez amount to emelletv.tez (tz1bQHQKT4BSoEreWKHuR3H5mme6fV3XCcvX)

-

Watch live at https://www.twitch.tv/emelletv

- diff --git a/data/planet/watch-ocaml/verifying-an-effect-based-cooperative-concurrency-scheduler-in-iris-by-adrian-dapprich.md b/data/planet/watch-ocaml/verifying-an-effect-based-cooperative-concurrency-scheduler-in-iris-by-adrian-dapprich.md deleted file mode 100644 index aec14923f2..0000000000 --- a/data/planet/watch-ocaml/verifying-an-effect-based-cooperative-concurrency-scheduler-in-iris-by-adrian-dapprich.md +++ /dev/null @@ -1,20 +0,0 @@ ---- -title: Verifying an Effect-Based Cooperative Concurrency Scheduler in Iris by Adrian - Dapprich -description: Lightweight asynchronous programming (using futures, goroutines or green - threads) has been widely adopted to organize programs with many concurrent tasks, - more than are traditionally feasible with ... -url: https://watch.ocaml.org/w/iQNqZzA8gVmd4RQaycAwx4 -date: 2024-01-09T16:23:50-00:00 -preview_image: https://watch.ocaml.org/lazy-static/previews/2f456a8e-7413-40c1-99c2-bf4f03b07887.jpg -authors: -- Watch OCaml -source: ---- - -

Lightweight asynchronous programming (using futures, goroutines or green threads) has been widely adopted to organize programs with many concurrent tasks, more than are traditionally feasible with thread-per-task models of concurrency.

-

With the release of OCaml 5 and its support for effect handlers, the new concurrency library Eio was proposed which aims to replace previous monadic concurrency libraries for OCaml.

-

In this work we verify the core fiber and promise abstractions of Eio and show their safety and effect safety using the Hazel program logic.

-

Hazel is built on the Iris framework and allows reasoning about programs with effect handlers. We also adapt the existing proof of the verified CQS datastructure since Eio uses a customized version of CQS for its implementation of promises.

-

We do not treat some features of Eio like cancellation, because it does not yield a verifiable specification, and resource control using switches, since it is a liveness property.

-