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
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 (74)
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
This page was built for publication: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
