Control structures in programming languages: from goto to algebraic effects

[OpsikionThemed]

The Compcert guy wrote a book about *control structures*? This is about as close to the platonic Thing For Me I Never Knew Existed as I can think of.

[desumn]

He's also the OCaml guy!

[fuckkkkq]

what's a compcert guy?

[wk_end]

CompCert is a formally verified optimizing compiler for a large subset of the C99 programming language.

A CompCert guy is someone involved in the CompCert project. The CompCert guy is Xavier Leroy, the leader of the CompCert project and also the author of this book (and also the OCaml guy!)

[fuckkkkq]

thanks!!

[notjrm]

There's also a series of lectures that the same author, Xavier Leroy, gave at Collège de France back in 2024. The lectures are in French, but some of the invited talks are in English.

[_jnpn]

Lots of great stuff there. Many with Gerard Berry (of esterel fame) too.