Effectful applicative similarity for call-by-name lambda calculi
type: Item
instance of: scholarly article
title: Effectful applicative similarity for call-by-name lambda calculi
zbMATH Open document ID: 1476.68052
author: Ugo Dal Lago
author: Francesco Gavazzo
author: Ryo Tanaka
published in: Theoretical Computer Science
publication date: 2020-04-21T00:00:00Z
full work available at URL: mainExtended.pdf
review text: The authors introduce and discuss a notion of equivalence of terms for a call-by-name lambda calculus with algebraic operations. This notion of applicative similarity is based on interpreting terms and operations as monadic values and is able to fully characterise contextual equivalence of terms (Corollary 1 on full abstraction). This contrasts with the usual notion of applicative similarity that interprets terms as values, but not monadic ones, and that does not satisfy full abstration with respect to contextual equivalence.
reviewed by: Danko Ilik
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 7191317
zbMATH Keywords: lambda calculus
zbMATH Keywords: algebraic effects
zbMATH Keywords: program equivalence
zbMATH Keywords: full abstraction
zbMATH Keywords: monads
MaRDI profile type: Publication
OpenAlex ID: W2999141155
cites work: Q4843177
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Step-Indexed Logical Relations for Probability
cites work: On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi
cites work: Q5144664
cites work: On coinductive equivalences for higher-order probabilistic functional programs
cites work: Q4692885
cites work: Nondeterministic extensions of untyped \(\lambda\)-calculus
cites work: RPO, Second-order Contexts, and Lambda-calculus
cites work: Logical relations for monadic types
cites work: Proving congruence of bisimulation in functional programming languages
cites work: Relational reasoning about contexts
cites work: Q5639839
cites work: Equivalence in functional languages with effects
cites work: Q3202991
cites work: Howe's method for higher-order languages
cites work: Q2771052
cites work: Algebraic operations and generic effects
cites work: Q5541339
Wikidata QID: Q126398608
DOI: 10.1016/J.TCS.2019.12.025
Recommended article: Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi
Recommended article: Applicative bisimilarities for call-by-name and call-by-value \(\lambda\mu\)-calculus
Recommended article: Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
Recommended article: Q5874223
Recommended article: A call-by-name lambda-calculus machine
Recommended article: Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus
Recommended article: Q4222771
Recommended article: Call-by-name, call-by-value, call-by-need and the linear lambda calculus
Recommended article: The Call-by-Need Lambda Calculus, Revisited
Recommended article: Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
description: scientific article; zbMATH DE number 7191317