31 citations · 39 across the 11 of their papers we have counts for
12 papers
Fully Abstract Encodings of -Calculus in HOcore through Abstract Machines
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet +3
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 se…
Automating the Functional Correspondence between Higher-Order Evaluators and Abstract Machines
Maciej Buszka, Dariusz Biernacki
The functional correspondence is a manual derivation technique transforming higher-order evaluators into the semantically equivalent abstract machines. The transformation consists…
An Abstract Machine for Strong Call by Value
Małgorzata Biernacka, Dariusz Biernacki, Witold Charatonik +1
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 correspon…
Bisimulations for Delimited-Control Operators
Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk
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 context…
Proving Soundness of Extensional Normal-Form Bisimilarities
Dariusz Biernacki, Serguei Lenglet, Piotr Polesiuk
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 t…
Logical relations for coherence of effect subtyping
Dariusz Biernacki, Piotr Polesiuk
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 semant…
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet +1
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. T…
Environmental Bisimulations for Delimited-Control Operators
Dariusz Biernacki, Sergueï Lenglet
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…
Proving termination of evaluation for System F with control operators
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet +1
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…
Normal Form Bisimulations for Delimited-Control Operators
Dariusz Biernacki, Serguei Lenglet
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 bisimilariti…
Applicative Bisimulations for Delimited-Control Operators
Dariusz Biernacki, Serguei Lenglet
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 possib…
An Operational Foundation for Delimited Continuations in the CPS Hierarchy
Malgorzata Biernacka, Dariusz Biernacki, Olivier Danvy
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. T…