Semantics of the typed -calculus with substitution in a cartesian closed category

DOI10.1016/0022-4049(93)90089-CMaRDI QIDQ687575zbMATH OpenFDO

Authors John W. Gray

Publication date 19 October 1993

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

zbMATH Keywords

semanticsoperational semanticsglobal environments objectindividual environments objectsinterpretation functiontyped \(\lambda\)-calculus with substitution

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Semantics in the theory of computing (68Q55)

Recommendations

• Simultaneous substitution in the typed lambda calculus
• scientific article; zbMATH DE number 3941502
• Simply typed lambda calculus with first-class environments
• scientific article; zbMATH DE number 1342289
• scientific article; zbMATH DE number 4010480

Cites work

• scientific article; zbMATH DE number 445156 (Why is no real title available?)
• scientific article; zbMATH DE number 3875278 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 19485 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3997132 (Why is no real title available?)
• Categorical combinators
• Explicit substitutions
• On specifications, theories, and models with higher types
• Simultaneous substitution in the typed lambda calculus

Cited in

(6)

• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• scientific article; zbMATH DE number 4010480 (Why is no real title available?)
• Simultaneous substitution in the typed lambda calculus
• Formal metatheory of the lambda calculus using Stoughton's substitution
• A semantics for \(\lambda_{str}^{\{\,\}}\): A calculus with overloading and late-binding
• An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus

This page was built for publication: Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q687575)