Distributive semantics for nondeterministic typed \(\lambda\)-calculi
type: Item
instance of: scholarly article
title: Distributive semantics for nondeterministic typed \(\lambda\)-calculi
zbMATH Open document ID: 0555.03007
DOI: 10.1016/0304-3975(84)90027-6
author: Egidio Astesiano
author: Gerardo Costa
published in: Theoretical Computer Science
publication date: 1984-01-01T00:00:00Z
review text: The paper presents a treatment of applicative languages based on the typed lambda-calculus enriched with a nondeterministic binary choice operator. The main aim of the paper is to give a semantics for the nondeterministic typed lambda-calculus which preserves the corresponding deterministic equivalences from the calculus without the nondeterministic choice operator. This aim is realized via giving an operational semantics of the calculus, using sharing technique preventing undesired duplicating of nondeterministic redexes, and the corresponding fully abstract (in the sense of Milner) denotational semantics, developing a theory of distributive models with the distributivity as the denotational counterpart of the sharing. The paper provides extensive motivations and the approach is exemplified on the language NDPCF.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3884132
zbMATH Keywords: nondeterministic languages
zbMATH Keywords: rewriting systems
zbMATH Keywords: fully abstract models
zbMATH Keywords: applicative languages
zbMATH Keywords: typed lambda-calculus
zbMATH Keywords: nondeterministic binary choice operator
zbMATH Keywords: operational semantics
zbMATH Keywords: denotational semantics
zbMATH Keywords: distributive models
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
full work available at URL: 0304-3975(84)90027-6
OpenAlex ID: W1996751264
cites work: Q4191570
cites work: Q3947101
cites work: Formal computations of non deterministic recursive program schemes
cites work: Q4139647
cites work: Q3206309
cites work: Q3912568
cites work: Q3912004
cites work: Parameter passing in nondeterministic recursive programs
cites work: Q3205213
cites work: Q4160405
cites work: Q3907039
cites work: Q4159365
cites work: A mathematical semantics for a nondeterministic typed lambda-calculus
cites work: The Semantics of Call-By-Value and Call-By-Name in a Nondeterministic Environment
cites work: Q3939778
cites work: Fully abstract models of typed \(\lambda\)-calculi
cites work: Q4051641
cites work: A Powerdomain Construction
cites work: LCF considered as a programming language
cites work: Q4195918
description: scientific article; zbMATH DE number 3884132