Levy: a Toy Call-by-Push-Value Language

Andrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml.

If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out.

It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more hands-on way to get to grips with CBPV would be to implement any of these missing features.

The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Too dense? No comments?

Too dense? No comments?

The authors of Levy admitted

The authors of Levy admitted they did not understand CBPV at first. How do I know if that is a correct implementation of it?

I got confused trying to match the language with the concepts in the book, that is probably only me.


I haven't played with it too much, but it seemed to fit more or less.

Which concepts are you talking about?


Regrettably, I haven't had time to dig into this in anything remotely resembling the depth it obviously deserves.