We are favonia and Flávio Cruz. This is our code for the Assignment 5 of 15-816 Linear Logic.
We implemented in Celf the operational semantics of Paul Blain Levy's call-by-push-value language extended with lazy substitution, mutable storable and limited forms of concurrency. For more information about the core language, see Call-By-Push-Value FAQ.