arXiv subjects

Dariusz Biernacki

Publications and source records attributed to Dariusz Biernacki.

12 recordsLinked to original sources

arXiv2024

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines

We present fully abstract encodings of the call-by-name and call-by-value $λ$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $λ$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and contextual equivalence -- that we internalize into abstract machines in order to prove full abstraction of the encodings. We also demonstrate that this technique scales to the $λμ$-calculus, i.e., a standard extension of the $λ$-calculus with control operators.

cs.LO↗

arXiv2021

Automating the Functional Correspondence between Higher-Order Evaluators and Abstract Machines

The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists of two well-known program transformations: translation to continuation-passing style that uncovers the control flow of the evaluator and Reynolds's defunctionalization that generates a first-order transition function. Ever since the transformation was first described by Danvy et al. it has found numerous applications in connecting known evaluators and abstract machines, but also in discovering new abstract machines for a variety of $λ$-calculi as well as for logic-programming, imperative and object-oriented languages. We present an algorithm that automates the functional correspondence. The algorithm accepts an evaluator written in a dedicated minimal functional meta-language and it first transforms it to administrative normal form, which facilitates program analysis, before performing selective translation to continuation-passing style, and selective defunctionalization. The two selective transformations are driven by a control-flow analysis that is computed by an abstract interpreter obtained using the abstracting abstract machines methodology, which makes it possible to transform only the desired parts of the evaluator. The article is accompanied by an implementation of the algorithm in the form of a command-line tool that allows for automatic transformation of an evaluator embedded in a Racket source file and gives fine-grained control over the resulting machine.

cs.PL↗

arXiv2020

An Abstract Machine for Strong Call by Value

We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $λ$-calculus. It is derived using Danvy et al.'s functional correspondence from Crégut's KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde's, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine. This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al.'s generalized refocusing. As a byproduct, we present an example application of the machine to checking term convertibility by discriminating on the basis of their partially normalized forms.

cs.PL↗

arXiv2019

Bisimulations for Delimited-Control Operators

We present a comprehensive study of the behavioral theory of an untyped $λ$-calculus extended with the delimited-control operators shift and reset. To that end, we define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We consider different styles of bisimilarities (namely applicative, normal-form, and environmental) within a unifying framework, and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.

cs.LO↗

arXiv2019

Proving Soundness of Extensional Normal-Form Bisimilarities

Normal-form bisimilarity is a simple, easy-to-use behavioral equivalence that relates terms in $λ$-calculi by decomposing their normal forms into bisimilar subterms. Moreover, it typically allows for powerful up-to techniques, such as bisimulation up to context, which simplify bisimulation proofs even further. However, proving soundness of these relations becomes complicated in the presence of $η$-expansion and usually relies on ad hoc proof methods which depend on the language. In this paper we propose a more systematic proof method to show that an extensional normal-form bisimilarity along with its corresponding up to context technique are sound. We illustrate our technique with three calculi: the call-by-value $λ$-calculus, the call-by-value $λ$-calculus with the delimited-control operators shift and reset, and the call-by-value $λ$-calculus with the abortive control operators call/cc and abort. In the first two cases, there was previously no sound up to context technique validating the $η$-law, whereas no theory of normal-form bisimulations for a calculus with call/cc and abort has been presented before. Our results have been fully formalized in the Coq proof assistant.

cs.LO↗

arXiv2018

Logical relations for coherence of effect subtyping

A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.

cs.PL↗

arXiv2017

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.

cs.PL↗

arXiv2013

Environmental Bisimulations for Delimited-Control Operators

We present a theory of environmental bisimilarity for the delimited-control operators {\it shift} and {\it reset}. We consider two different notions of contextual equivalence: one that does not require the presence of a top-level control delimiter when executing tested terms, and another one, fully compatible with the original CPS semantics of shift and reset, that does. For each of them, we develop sound and complete environmental bisimilarities, and we discuss up-to techniques.

cs.PL↗

arXiv2013

Proving termination of evaluation for System F with control operators

We present new proofs of termination of evaluation in reduction semantics (i.e., a small-step operational semantics with explicit representation of evaluation contexts) for System F with control operators. We introduce a modified version of Girard's proof method based on reducibility candidates, where the reducibility predicates are defined on values and on evaluation contexts as prescribed by the reduction semantics format. We address both abortive control operators (callcc) and delimited-control operators (shift and reset) for which we introduce novel polymorphic type systems, and we consider both the call-by-value and call-by-name evaluation strategies.

cs.PL↗

arXiv2012

Normal Form Bisimulations for Delimited-Control Operators

We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.

cs.PL↗

arXiv2012

Applicative Bisimulations for Delimited-Control Operators

We develop a behavioral theory for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. For this calculus, we discuss the possible observable behaviors and we define an applicative bisimilarity that characterizes contextual equivalence. We then compare the applicative bisimilarity and the CPS equivalence, a relation on terms often used in studies of control operators. In the process, we illustrate how bisimilarity can be used to prove equivalence of terms with delimited-control effects.

cs.PL↗

arXiv2005

An Operational Foundation for Delimited Continuations in the CPS Hierarchy

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 hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

cs.LO↗