Landin's Knot is diagnosed as an effect of impredicative environment quantification, and a universe-stratified reference rule is conjectured to restore strong normalization without linear types.
A monad for full ground reference cells
1 Pith paper cite this work. Polarity classification is still indexing.
abstract
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.
citation-role summary
citation-polarity summary
fields
cs.PL 1years
2025 1verdicts
CONDITIONAL 1roles
background 1polarities
unclear 1representative citing papers
citing papers explorer
-
One Weird Trick to Untie Landin's Knot
Landin's Knot is diagnosed as an effect of impredicative environment quantification, and a universe-stratified reference rule is conjectured to restore strong normalization without linear types.