Effectful applicative similarity for call-by-name lambda calculi

DOI10.1016/j.tcs.2019.12.025zbMath1476.68052OpenAlexW2999141155WikidataQ126398608 ScholiaQ126398608MaRDI QIDQ1989333

Ugo Dal Lago, Francesco Gavazzo, Ryo Tanaka

Publication date: 21 April 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-02991694/file/mainExtended.pdf

zbMATH Keywords

full abstractionmonadslambda calculusalgebraic effectsprogram equivalence

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Algebraic operations and generic effects
• Proving congruence of bisimulation in functional programming languages
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Step-Indexed Logical Relations for Probability
• RPO, Second-order Contexts, and Lambda-calculus
• Logical relations for monadic types
• Equivalence in functional languages with effects
• On coinductive equivalences for higher-order probabilistic functional programs
• On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi
• Howe's method for higher-order languages