Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
5 results

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 $\lambda$-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&nbsp;[&hellip;]
Published on March 29, 2019

Bisimulations for Delimited-Control Operators

Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk.
We present a comprehensive study of the behavioral theory of an untyped $\lambda$-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&nbsp;[&hellip;]
Published on May 24, 2019

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Andrés Aristizábal ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk.
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&nbsp;[&hellip;]
Published on September 19, 2017

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 semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article&nbsp;[&hellip;]
Published on January 30, 2018

Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines

Małgorzata Biernacka ; Dariusz Biernacki ; Sergueï Lenglet ; Piotr Polesiuk ; Damien Pous ; Alan Schmitt.
We present fully abstract encodings of the call-by-name and call-by-value $\lambda$-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the $\lambda$-calculus side -- normal-form bisimilarity, applicative bisimilarity, and&nbsp;[&hellip;]
Published on July 3, 2024

  • < Previous
  • 1
  • Next >