scientific article; zbMATH DE number 5318491

zbMATH Open1149.03016MaRDI QIDQ3522248FDOQ3522248

Authors: Jonathan P. Seldin, J. Roger Hindley 

Publication date: 1 September 2008

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 3993540
• scientific article; zbMATH DE number 4002064
• The lambda calculus. Its syntax and semantics. Rev. ed.
• scientific article; zbMATH DE number 3875232
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• scientific article; zbMATH DE number 2242116
• scientific article; zbMATH DE number 32501
• scientific article; zbMATH DE number 5852776
• scientific article; zbMATH DE number 4024773

zbMATH Keywords

combinatory logictype theorylambda calculuscombinator

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01)

Cited In (69)

• Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
• Towards a homotopy domain theory
• Title not available (Why is that?)
• A formal system of reduction paths for parallel reduction
• Title not available (Why is that?)
• Lambda calculus with patterns
• Title not available (Why is that?)
• Bounded combinatory logic and lower complexity
• Algebraic and Logical Operations on Operators One Application to Semantic Computation
• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Mockingbird lattices
• The IO and OI hierarchies revisited
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• A simplified proof of the Church-Rosser theorem
• The Church-Rosser theorem and quantitative analysis of witnesses
• Title not available (Why is that?)
• The broadest necessity
• Strong reduction of combinatory calculus with streams
• Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey
• A combinator-based superposition calculus for higher-order logic
• Lambda terms definable as combinators
• Combinatory logic. Pure, applied and typed
• Combinatory logic with polymorphic types
• Title not available (Why is that?)
• A solution to Curry and Hindley's problem on combinatory strong reduction
• Models of the lambda calculus: an introduction
• Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer)
• Title not available (Why is that?)
• Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms
• A Short Introduction to Implicit Computational Complexity
• Title not available (Why is that?)
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Reduction rules for intuitionistic \(\lambda\rho\)-calculus
• Bridging Curry and Church's typing style
• Unifying Math Ontologies: A Tale of Two Standards
• A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
• Bunder's paradox
• Title not available (Why is that?)
• Barendregt's problem \#26 and combinatory strong reduction
• Constructibility and Geometry
• Title not available (Why is that?)
• Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
• A Nominal Axiomatization of the Lambda Calculus
• Verificationism and Classical Realizability
• The Scott model of PCF in univalent type theory
• Title not available (Why is that?)
• The search for a reduction in combinatory logic equivalent to \(\lambda \beta\)-reduction. II.
• Title not available (Why is that?)
• A decidable theory of type assignment
• Book review of: H. Barendregt et al., Lambda calculus with types
• The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction
• Structure by proxy, with an application to grounding
• A theory of necessities
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• An Introduction to the Lambda Calculus
• Imaginary groups: lazy monoids and reversible computation
• A Knuth-Bendix-like ordering for orienting combinator equations
• The functional interpretation of direct computations
• Clocks for Functional Programs
• A (machine-oriented) logic based on pattern matching
• A lambda calculus satellite
• Logical predicates in higher-order mathematical operational semantics
• Core Type Theory
• Lower end of the linial-post spectrum
• The combinator M and the Mockingbird lattice
• Puzzles of existential generalisation from type-theoretic perspective
• A century since \textit{Principia}'s substitution bedazzled Haskell Curry. In honour of Jonathan Seldin's 80th anniversary
• A Formal Proof of the Strong Normalization Theorem for System T in Agda

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522248)