scientific article
From MaRDI portal
Publication:3522248
zbMath1149.03016MaRDI QIDQ3522248
Jonathan P. Seldin, J. Roger Hindley
Publication date: 1 September 2008
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
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) Combinatory logic and lambda calculus (03B40)
Related Items (48)
Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer) ⋮ Bounded combinatory logic and lower complexity ⋮ A Short Introduction to Implicit Computational Complexity ⋮ The Church-Rosser theorem and quantitative analysis of witnesses ⋮ The broadest necessity ⋮ The Scott model of PCF in univalent type theory ⋮ Combinatory logic with polymorphic types ⋮ The combinator M and the Mockingbird lattice ⋮ Bridging Curry and Church's typing style ⋮ Lambda calculus with types (Perspectives in Logic) ⋮ A decidable theory of type assignment ⋮ Typing Weak MSOL Properties ⋮ Unnamed Item ⋮ Algebraic and Logical Operations on Operators One Application to Semantic Computation ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Mockingbird lattices ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ Reduction rules for intuitionistic \(\lambda\rho\)-calculus ⋮ A (machine-oriented) logic based on pattern matching ⋮ Core Type Theory ⋮ Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers ⋮ Structure by proxy, with an application to grounding ⋮ Towards a homotopy domain theory ⋮ Unnamed Item ⋮ The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction ⋮ Verificationism and Classical Realizability ⋮ Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey ⋮ Imaginary groups: lazy monoids and reversible computation ⋮ The search for a reduction in combinatory logic equivalent to \(\lambda \beta\)-reduction. II. ⋮ A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language ⋮ A formal system of reduction paths for parallel reduction ⋮ Clocks for Functional Programs ⋮ The Functional Interpretation of Direct Computations ⋮ A simplified proof of the Church-Rosser theorem ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Constructibility and Geometry ⋮ A solution to Curry and Hindley's problem on combinatory strong reduction ⋮ BUNDER’S PARADOX ⋮ Unifying Math Ontologies: A Tale of Two Standards ⋮ Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms ⋮ A theory of necessities ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Barendregt's problem \#26 and combinatory strong reduction ⋮ The IO and OI hierarchies revisited ⋮ Strong reduction of combinatory calculus with streams
This page was built for publication:
