From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models

DOI10.1016/S0304-3975(00)00057-8zbMath0949.68049OpenAlexW1974315746MaRDI QIDQ1583485

Chantal Berline

Publication date: 26 October 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00057-8

zbMATH Keywords

calculusgraph modelsmap theoryequational extensions of calculusmodels of untyped calculuswebbed models

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (16)

Easy lambda-terms are not always simple ⋮ Relational graph models, Taylor expansion and extensionality ⋮ Graph easy sets of mute lambda terms ⋮ Easiness in graph models ⋮ Unnamed Item ⋮ A relational semantics for parallelism and non-determinism in a functional setting ⋮ A synthetic axiomatization of map theory ⋮ Graph lambda theories ⋮ An irregular filter model ⋮ Some reasons for generalising domain theory ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ A Relational Model of a Parallel and Non-deterministic λ-Calculus ⋮ Unnamed Item ⋮ Effective λ-models versus recursively enumerable λ-theories ⋮ Building continuous webbed models for system F ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types

Cites Work

• Forcing in stable models of untyped \(\lambda\)-calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• A characterization of F-complete type assignments
• The system \({\mathcal F}\) of variable types, fifteen years later
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• A type-free system extending (ZFC)
• Strong stability and the incompleteness of stable models for \(\lambda\)-calculus
• A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\)
• Set theory. An introduction to independence proofs
• Petri nets, event structures and domains. I
• Domain theory in logical form
• Classical recursion theory. The theory of functions and sets of natural numbers
• Map theory
• Complete restrictions of the intersection type discipline
• An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• LCF considered as a programming language
• Full abstraction in the lazy lambda calculus
• Infinite \(\lambda\)-calculus and types
• Lambda-calculi for (strict) parallel functions
• Some new results on easy lambda-terms
• A semantics for static type inference
• Classical logic, storage operators and second-order lambda-calculus
• A syntactical proof of the operational equivalence of two \(\lambda\)-terms
• Isomorphism and equational equivalence of continuous \(\lambda\)-models
• A theory of sequentiality
• About classical logic and imperative programming
• A set of postulates for the foundation of logic. II
• Consistency of a \(\lambda\)-theory with \(n\)-tuples and easy term
• Universal retractions on \(DI\)-domains
• The inconsistency of certain formal logics
• A filter lambda model and the completeness of type assignment
• Isomorphisms and nonisomorphisms of graph models
• The Expressiveness of Simple and Second-Order Type Structures
• Toward useful type-free theories. I
• A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
• Data Types as Lattices
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Can programming be liberated from the von Neumann style?
• Approximate Reduction and Lambda Calculus Models
• The interpretation of unsolvable λ-terms in models of untyped λ-calculus
• The Impact of the Lambda Calculus in Logic and Computer Science
• Functionality in Combinatory Logic
• Origins of Recursive Function Theory
• The Mechanical Evaluation of Expressions
• A \(\kappa\)-denotational semantics for map theory in ZFC+SI
• On the construction of stable models of untyped \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models