The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
From MaRDI portal
Publication:4115133
DOI10.1137/0205036zbMath0346.02013MaRDI QIDQ4115133
Publication date: 1976
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/0205036
03B40: Combinatory logic and lambda calculus
Related Items
A domain-theoretic approach to functional and logic programming, Call-by-value Solvability, Intersection types for \(\lambda\)-trees, Innocent game models of untyped \(\lambda\)-calculus, On the construction of stable models of untyped \(\lambda\)-calculus, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Filter models for conjunctive-disjunctive \(\lambda\)-calculi, Uniqueness of Scott's reflexive domain in \(P\omega \), Type inference with recursive types: Syntax and semantics, Semantics of algorithmic languages, Expressive power of typed and type-free programming languages, The insensitivity theorem for nonreducing reflexive types, Parametric \(\lambda \)-theories, The heart of intersection type assignment: Normalisation proofs revisited, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, A characterization of F-complete type assignments, Recursively defined domains and their induction principles, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, Substitution revisited, Polymorphic type inference and containment, Strictness analysis of the untyped \(\lambda\)-calculus, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Full abstraction and limiting completeness in equational languages, \(\mathbb{T}^\omega\) as a universal domain, The IO- and OI-hierarchies, Sequential algorithms on concrete data structures, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, Intersection types for combinatory logic, Fully abstract models of typed \(\lambda\)-calculi, A discrimination algorithm inside \(\lambda -\beta\)-calculus, Type inference with partial types, Intersection type assignment systems, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, Intersection types and domain operators, On the semantics of the call-by-name CPS transform, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, On infinite \(\eta\)-expansion, Typing and computational properties of lambda expressions, Approximation properties of abstract data types, Normalization, approximation, and semantics for combinator systems, Infinitary lambda calculus and discrimination of Berarducci trees., The origins of structural operational semantics, Order-incompleteness and finite lambda reduction models, Relating graph and term rewriting via Böhm models, Easiness in graph models, State-transition machines for lambda-calculus expressions, State-transition machines, revisited, Unnamed Item, Unnamed Item, Completeness of transfinite evaluation in an extension of the lambda calculus, European meeting of the Association for Symbolic Logic, Mons, Belgium, 1978, Degrees of sensible lambda theories, Upper bounds for standardizations and an application
