Reynolds's defunctionalization technique is a whole-program transformation from higher-
order to first-order functional programs. We study practical applications of this transformation …

It is well-known that many environment-based abstract machines can be seen as strategies
in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear …

In CSL-LICS 2014, Accattoli and Dal Lago [1] showed that there is an implementation of the
ordinary (ie strong, pure, call-by-name) λ-calculus into models like RAM machines which is …

This document illustrates how functional implementations of formal semantics (structural
operational semantics, reduction semantics, small-step and big-step abstract machines …

First-class control operators provide programmers with an expressive and efficient means for
manipulating control through reification of the current control state as a first-class object …

We present an abstract machine and a reduction semantics for the lambda-calculus
extended with control operators that give access to delimited continuations in the CPS …

We present a type system with subtyping for first-class delimited continuations that
generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit …

We document an operational method to construct reduction-free normalization functions.
Starting from a reduction-based normalization function from a reduction semantics, ie, the …

We present a systematic construction of environment-based abstract machines from context-
sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for …

Using a stack for managing the local state of procedures as popularized by Algol is a simple
but effective way to achieve a primitive form of automatic memory management. Hence, the …