Great paper, thanks for sharing! The connection between programming language technology and formal logic, like here for sequent calculus, is one of the most fas

Great paper, thanks for sharing! The connection between programming language technology and formal logic, like here for sequent calculus, is one of the most fascinating things. For anyone who struggles with the references to \lambda-\mu-\tilde{\mu}, the notion that a continuation takes multiple arguments and that "control effects arise naturally", it may be helpful to review the CEK machine first: https://burakemir.ch/post/cek-and-control/ https://burakemir.ch/post/cek-and-control/