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.02013OpenAlexW2184268586MaRDI QIDQ4115133

Christopher P. Wadsworth

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



Related Items

Infinitary lambda calculus and discrimination of Berarducci trees., Upper bounds for standardizations and an application, The origins of structural operational semantics, Easiness in graph models, Order-incompleteness and finite lambda reduction models, A characterization of F-complete type assignments, Algebraic semantics and complexity of term rewriting systems, Intersection type assignment systems, Recursively defined domains and their induction principles, A General Class of Models of $\mathcal{H}^*$, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, Substitution revisited, Polymorphic type inference and containment, Strictness analysis of the untyped \(\lambda\)-calculus, Unnamed Item, A class of bounded functions, a database language and an extended 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, Relating graph and term rewriting via Böhm models, Semantic types and approximation for Featherweight Java, \(\mathbb{T}^\omega\) as a universal domain, Intersection and union types, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, Completeness of transfinite evaluation in an extension of the lambda calculus, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, The IO- and OI-hierarchies, Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation, Sequential algorithms on concrete data structures, Parametric \(\lambda \)-theories, The heart of intersection type assignment: Normalisation proofs revisited, Intersection types and domain operators, Filter models for conjunctive-disjunctive \(\lambda\)-calculi, Uniqueness of Scott's reflexive domain in \(P\omega \), State-transition machines for lambda-calculus expressions, State-transition machines, revisited, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Unnamed Item, Approximation and normalization results for typeable term rewriting systems, Functional Type Assignment for Featherweight Java, An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus, Intersection types for combinatory logic, From Böhm's Theorem to Observational Equivalences, Strong normalization from an unusual point of view, Cut-elimination in the strict intersection type assignment system is strongly normalizing, European meeting of the Association for Symbolic Logic, Mons, Belgium, 1978, Intersection types for \(\lambda\)-trees, Innocent game models of untyped \(\lambda\)-calculus, On the construction of stable models of untyped \(\lambda\)-calculus, Call-by-value Solvability, Unnamed Item, Fully abstract models of typed \(\lambda\)-calculi, Unnamed Item, Unnamed Item, Relating graph and term rewriting via Böhm models, Unnamed Item, A discrimination algorithm inside \(\lambda -\beta\)-calculus, Type inference with recursive types: Syntax and semantics, Typing and computational properties of lambda expressions, Degrees of sensible lambda theories, Semantics of algorithmic languages, Expressive power of typed and type-free programming languages, On the semantics of the call-by-name CPS transform, Strongly Normalising Cut-Elimination with Strict Intersection Types, Approximation properties of abstract data types, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Unnamed Item, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, The insensitivity theorem for nonreducing reflexive types, Normalization, approximation, and semantics for combinator systems, Definability and Full Abstraction, On infinite \(\eta\)-expansion, A domain-theoretic approach to functional and logic programming, Type inference with partial types, The infinitary lambda calculus of the infinite eta Böhm trees