The lambda calculus, its syntax and semantics
From MaRDI portal
Publication:1155602
zbMath0467.03010MaRDI QIDQ1155602
Publication date: 1981
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Computability and recursion theory (03D99) Combinatory logic and lambda calculus (03B40)
Related Items (only showing first 100 items - show all)
Extended term rewriting systems ⋮ Explicit effect subtyping ⋮ Levy Labels and Recursive Types ⋮ On the \(\lambda Y\) calculus ⋮ Parametric parameter passing \(\lambda\)-calculus ⋮ Enumerators of lambda terms are reducing constructively ⋮ Adding algebraic rewriting to the untyped lambda calculus (extended abstract) ⋮ Some lambda calculi with categorical sums and products ⋮ Proving the genericity lemma by leftmost reduction is simple ⋮ The combinator M and the Mockingbird lattice ⋮ Universal domains and the amalgamation property ⋮ Levels of truth ⋮ NP-completeness of a combinator optimization problem ⋮ Using resolution for deciding solvable classes and building finite models ⋮ On λ-Definable Functions on Ordinals ⋮ Unnamed Item ⋮ Polymorphic extensions of simple type structures. With an application to a bar recursive minimization ⋮ Embedding of a free cartesian-closed category into the category of sets ⋮ Functions as processes ⋮ Meeting of the Association for Symbolic Logic, Stanford, California, 1985 ⋮ Wrapper semantics of an object-oriented programming language with state ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ A first order logic of effects ⋮ A confluent calculus for concurrent constraint programming ⋮ Developing developments ⋮ Higher-order subtyping ⋮ A user's friendly syntax to define recursive functions as typed λ-terms ⋮ A short and flexible proof of strong normalization for the calculus of constructions ⋮ The Maude strategy language ⋮ A simple language supporting angelic nondeterminism and parallel composition ⋮ Correctness of procedure representations in higher-order assembly language ⋮ A deterministic rewrite system for the probabilistic λ-calculus ⋮ A linear logical framework ⋮ Many more predecessors: A representation workout ⋮ The conservation theorem for differential nets ⋮ SAC -- a functional array language for efficient multi-threaded execution ⋮ Point-fixe sur un ensemble restreint ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Three faces of natural deduction ⋮ Proposal for a natural formalization of functional programming concepts ⋮ Variations on mobile processes ⋮ Psi-calculi in Isabelle ⋮ On Higher-Order Probabilistic Subrecursion ⋮ Strategic port graph rewriting: an interactive modelling framework ⋮ Improving the lazy Krivine machine ⋮ Strongly reducing variants of the Krivine abstract machine ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Unnamed Item ⋮ Decidability of all minimal models ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ A higher-order strategy for eliminating common subexpressions ⋮ The Typed Böhm Theorem ⋮ Hyperformulae, Parallel Deductions and Intersection Types ⋮ Alonzo church:his life, his work and some of his miracles ⋮ Classical \(F_{\omega}\), orthogonality and symmetric candidates ⋮ A \(\kappa\)-denotational semantics for map theory in ZFC+SI ⋮ Pure bigraphs: structure and dynamics ⋮ Formal SOS-Proofs for the Lambda-Calculus ⋮ The Functional Interpretation of Direct Computations ⋮ Equivalence in functional languages with effects ⋮ Introduction to Type Theory ⋮ Dependent vector types for data structuring in multirate Faust ⋮ Unnamed Item ⋮ Automated reasoning contributes to mathematics and logic ⋮ SPACE AND TIME IN COMPUTATION AND DISCRETE PHYSICS ⋮ Translating between Language and Logic: What Is Easy and What Is Difficult ⋮ Unnamed Item ⋮ On Fixed Point Theory and Its Applications to Equilibrium Models ⋮ A theory of rules for enumerated classes of functions ⋮ Russell's 1903 - 1905 Anticipation of the Lambda Calculus ⋮ COCHIS: Stable and coherent implicits ⋮ A semantical proof of De Jongh's theorem ⋮ Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus ⋮ Typing and computational properties of lambda expressions ⋮ Self-similar sets as Tarski's fixed points ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ On the logic of unification ⋮ Towards a computation system based on set theory ⋮ Sequential evaluation strategies for parallel-or and related reduction systems ⋮ Evolving combinators ⋮ A normalization theorem for set theory ⋮ Dedekind completion as a method for constructing new Scott domains ⋮ On the semantics of polymorphism ⋮ Reduction of finite and infinite derivations ⋮ On principal types of combinators ⋮ Diagonal fixed points in algebraic recursion theory ⋮ Equality between functionals in the presence of coproducts ⋮ Integration in Real PCF ⋮ Theoretical Pearl Yet yet a counterexample for λ+SP ⋮ Total unfolding: theory and applications ⋮ On a Fully Abstract Model for a Quantum Linear Functional Language ⋮ Classical lambda calculus in modern dress ⋮ Computing in unpredictable environments: Semantics, reduction strategies, and program transformations ⋮ Structured algebraic specifications: A kernel language ⋮ When is partial trace equivalence adequate? ⋮ Partial evaluation and \(\omega\)-completeness of algebraic specifications ⋮ Third order matching is decidable ⋮ Regular expressions with nested levels of back referencing form a hierarchy ⋮ Universal profinite domains
This page was built for publication: The lambda calculus, its syntax and semantics
