arXiv subjects

Piotr Polesiuk

Publications and source records attributed to Piotr Polesiuk.

7 recordsLinked to original sources

arXiv2026

Remarks on Algebraic Reconstruction of Types and Effects

In their 1991 paper "Algebraic Reconstruction of Types and Effects," Pierre Jouvelot and David Gifford presented a type-and-effect reconstruction algorithm based on an algebraic structure of effects. Their work is considered a milestone in the development of type-and-effect systems, and has inspired numerous subsequent works in the area of static analysis. However, unlike the later research it spawned, the original algorithm considered a language with higher-rank polymorphism, a feature which is challenging to implement correctly. In this note, we identify subtle bugs related to variable binding in their approach to this feature. We revisit their type system and reconstruction algorithm, and describe the discovered issues.

cs.PL↗

arXiv2025

Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism

Type-and-effect systems help the programmer to organize data and computational effects in a program. While for traditional type systems expressive variants with sophisticated inference algorithms have been developed and widely used in programming languages, type-and-effect systems did not yet gain widespread adoption. One reason for this is that type-and-effect systems are more complex and the existing inference algorithms make compromises between expressiveness, intuitiveness, and decidability. In this work, we present an effect inference algorithm for a type-and-effect system with subtyping, expressive higher-rank polymorphism, and intuitive set-like semantics of effects. In order to deal with scoping issues of higher-rank polymorphism, we delay solving of effect constraints by transforming them into formulae of propositional logic. We prove soundness and completeness of our algorithm with respect to a declarative type-and-effect system. All the presented results have been formalized in the Rocq proof assistant, and the algorithm has been successfully implemented in a realistic programming language.

cs.PL↗

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↗

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↗