7 papers
Remarks on Algebraic Reconstruction of Types and Effects
Patrycja Balik, Szymon Jędras, Piotr Polesiuk
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 st…
Deciding not to Decide: Sound and Complete Effect Inference in the Presence of Higher-Rank Polymorphism
Patrycja Balik, Szymon Jędras, Piotr Polesiuk
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 infer…
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…
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…