An algebraic stepper is a pedagogical tool for showing the intermediate steps of program execution. This paper presents an algebraic stepper for OCaml that supports simple modules with hierarchical reference to variables (but without functors or signature sealing). When we program with modules, we can refer to a variable declared in a parent module directly, whereas we need to specify a module path to refer to a variable declared in a child module. Therefore, when we build the stepper, we attach a level to each variable (bound by let statement without in) and use it to maintain correct reference regardless of where a variable is used. In this paper, we present and formalize our stepper that implements delayed substitution of variables, and discuss the interplay between the stepper semantics and the level maintenance. We further show that the execution in the stepper semantics is consistent with the one in the standard small-step semantics. The resulting stepper is implemented, supporting most of the basic constructs of OCaml, and is used in an introductory OCaml course in the authors' institution.

Abstract OCaml Blockly is a block-based programming environment for a subset of the functional language OCaml, developed based on Google Blockly. The distinct feature of OCaml Blockly is that it knows the scoping and typing rules of OCaml. As such, for any complete program in OCaml Blockly, its OCaml counterpart compiles: it is free from syntax errors, scoping errors, and type errors. OCaml Blockly supports introductory constructs of OCaml that are sufficient to write the shortest path problem for the Tokyo metro network. This paper describes the design of OCaml Blockly and how it is used in a CS-major course on functional programming.

The operational behavior of control operators has been studied comprehensively in the past few decades, but type systems of control operators have not. There are distinct type systems for shift, control, and shift0 without any relationship between them, and there has not been a type system that directly corresponds to control0. This paper remedies this situation by giving a uniform type system for all the four control operators. Following Danvy and Filinski’s approach, we derive a monomorphic type system from the CPS interpreter that defines the operational semantics of the four control operators. By implementing the typed CPS interpreter in Agda, we show that the CPS translation preserves types and that the calculus with all the four control operators is terminating. Furthermore, we show the relationship between our type system and the previous type systems for shift, control, and shift0.

In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a monomorphic type system of the shift and reset operators from a CPS semantics. In this paper, we show how this method scales to Felleisen's control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of previously captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS semantics, we can derive a type system that encodes all and only constraints imposed by the CPS semantics.

This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.

This paper presents a selective CPS transformation for a program that uses control operators, shift and reset, introduced by Danvy and Filinski. By selectively CPS-transforming a program, we can execute a program with shift and reset in a standard functional language without support for control operators. We introduce a constraint-based type inference system that annotates the parts that are captured by shift and thus require CPS transformation. We show that the best annotation does not exist in general, and present a constraint solving algorithm that is reasonably efficient. The selective CPS transformation is defined over annotated terms and its correctness is proven. Finally, experimental results show that selective CPS transformation does improve performance compared to the standard CPS transformation.

Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been put into enriching dependently typed languages with missing constructs, most notably, effects. This paper presents a language that has two practically interesting ingredients: dependent inductive types, and the delimited control constructs shift and reset. When integrating delimited control into a dependently typed language, however, two challenges arise. First, the dynamic nature of control operators, which is the source of their expressiveness, can break fundamental language properties such as logical consistency and subject reduction. Second, CPS translations, which we often use to define the semantics of control operators, do not scale straightforwardly to dependently typed languages. We solve the former issue by restricting dependency of types, and the latter using answer-type polymorphism of pure terms. The main contribution of this paper is to give a sound type system of our language, as well as a type-preserving CPS translation. We also discuss various extensions, which would make our language more like a full-spectrum proof assistant but pose non-trivial issues.

This paper relates 2-level lambda-calculus and staged lambda-calculus (restricted to 2 stages) to obtain monovariant binding-time analysis for lambda-calculus that produces the output in the form of staging annotations. The relationship between the two lambda-calculi provides us with a precise and easy instruction on how to implement binding-time analysis to be incorporated in the staged lambda-calculus. It forms a basis for introducing binding-time analysis to full-fledged staged languages such as MetaOCaml.

A reflective language makes the language semantics open to user programs and allows them to access, extend, and modify it from within the same language framework. Because of its high flexibility and expressiveness, it can be an ideal platform for programming language research as well as practical applications in dynamic environments. However, efficient implementation of a reflective language is extremely difficult. Under the circumstance where the language semantics can change, a partial evaluator is required for compilation. This paper reports on the experience of using MetaOCaml as a compiler for a reflective language. With staging annotations, MetaOCaml achieves the same effect as using a partial evaluator. Unlike the standard partial evaluator, the run mechanism of MetaOCaml enables us to use the specialized (compiled) code in the current runtime environment. On the other hand, the lack of a binding-time analysis in MetaOCaml prohibits us from compiling a user program under modified compiled semantics.

We develop a type theoretic specification of offline partial evaluation for the simply-typed lambda calculus in the dependently-typed programming language Agda. We establish the correctness of the specification by proving termination, typing preservation, and semantics preservation using logical relations. Typing preservation is achieved by relying on a typed syntax representation based on De Bruijn indices for the source and the target language. The full calculus contains primitive recursion on natural numbers and higher-order lifting for function, product, and sum types.

The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 19–21, 2011 in Tokyo, Japan. After the conference, the programme committee, chaired by Olivier Danvy, selected several outstanding papers and invited their authors to submit to this special issue of the Journal of Functional Programming . Kenichi Asai and Benjamin C. Pierce acted as editors for these submissions. This issue includes the three accepted articles, each of which provides substantial new material beyond the original conference version. The selected papers represent the importance of various aspects of proof techniques, from theory to practice, all of which aim at verifying realistic programs.

A reflective language enables us to access, inspect, and/or modify the language semantics from within the same language framework. Although the degree of semantics exposure differs from one language to another, the most powerful approach, referred to as the behavioral reflection, exposes the entire language semantics (or the language interpreter) that defines behavior of user programs for user inspection/modification. In this paper, we deal with the behavioral reflection in the context of a functional language Scheme. In particular, we show how to construct a reflective interpreter where user programs are interpreted by the tower of metacircular interpreters and have the ability to change any parts of the interpreters during execution. Its distinctive feature compared to the previous work is that the metalevel interpreters observed by users are written in direct style. Based on the past attempt of the present author, the current work solves the level-shifting anomaly by defunctionalizing and inspecting the top of the continuation frames. The resulting system enables us to freely go up and down the levels and access/modify the direct-style metalevel interpreter. This is in contrast to the previous system where metalevel interpreters were written in continuation-passing style (CPS) and only CPS functions could be exposed to users for modification.

This paper connects the definitional interpreter for the λ-calculus extended with delimited continuation constructs, shift and reset, with a compiler and a low-level virtual machine that copies a part of a data stack to implement delimited continuations. Following the functional derivation approach proposed and popularized by Danvy, we interrelate the two implementations via a series of meaning-preserving program transformations whose validity is independently known. As a result, this work formally establishes the correctness of a compiler and a low-level stack-copying implementation of delimited continuations. In particular, the resulting virtual machine properly models when to store return addresses into a data stack and which part of a data stack to copy. To our knowledge, this work is the first to prove correctness of such low-level features of delimited continuations. It also shows that the functional derivation approach is equally applicable to establish correctness of low-level implementations.

This paper presents an offline partial evaluator for the λ-calculus with the delimited continuation constructs shift and reset. Based on Danvy and Filinski's type system for shift and reset, we first present a type system that specifies well-annotated terms. We then show a specializer that receives an annotated term and produces the output in continuation-passing style (CPS). The correctness of our partial evaluator is established using the technique of logical relations. Thanks to the explicit reference to the type of continuations, we can establish the correctness using the standard proof technique of structural induction, despite the fact that the specializer itself is written in CPS. The paper also shows an efficient constraint-based binding-time analysis as well as how to extend the present work to richer language constructs, such as recursion and conditionals.

This paper presents an online partial evaluator for the λ-calculus with the delimited continuation constructs shift and reset. We first give the semantics of the delimited continuation constructs in two ways: one by writing a continuation passing style (CPS) interpreter and the other by transforming them into CPS. We then combine them to obtain a partial evaluator written in CPS which produces the result in CPS. By transforming this partial evaluator back into a direct style (DS) in two steps, we obtain a DS to DS partial evaluator written in DS. The correctness of the partial evaluator is not yet formally proven. The difficulty comes from the fact that the partial evaluator is written using shift and reset. The method for reasoning about such programs is not yet established. However, the development of the partial evaluator is detailed in the paper to give a degree of confidence that it behaves as we expect.

We present a framework of an online partial evaluator for a call-by-value λ-calculus with destructive updates of data structures. It properly and correctly specializes expressions that contain side-effects, while preserving pointer equality, which is an important property for programs using updates. Our partial evaluator uses a side-effect analysis to extract immutable data structures and then performs an online specialization using preactions. Once mutable and immutable data structures are separated, partial evaluation is done in such a way that accesses to immutable ones are performed at specialization time, while accesses to mutable ones are residualized. For the correct residualization of side-effecting operations, preactions are used to solve various issues, including code elimination, code duplication, and execution order preservation. The preaction mechanism also enables us to reduce expressions that were residualized when the conventional let-expression approach of Similix was used. The resulting partial evaluator is simple enough to prove its correctness. Based on the framework, we have constructed a partial evaluator for Scheme, which is powerful enough to specialize fairly complicated programs with side-effects, such as an interpreter.

Meta-level programmability is beneficial for parallel/distributed object-oriented computing to improve performance, etc. The major problem, however, is interpretation overhead due to mta-circular interpretation. To solve this problem, we propose a compilation framework for object-oriented concurrent reflective languages using partial evaluation. Since traditional partial evaluators do not allow us to directly deal with meta-circular interpreters written with concurrent objects, we devised techniques such as pre-/post-processing, a new proposed preaction extension to partial evaluation in order to handle side-effects, etc. Benchmarks of a prototype compiler for our language ABCL/R3 indicate that (1) the meta-level interpretation is essentially 'compiled away,' and (2) mta-level optimizations in a parallel application, running on a Fujitsu MPP AP1000, exhibits only 10--30% overhead compared to the hand-crafted source-level optimization in a non-reflective language.