Combinatory logic. With two sections by William Craig.
From MaRDI portal
Publication:769601
zbMath0081.24104MaRDI QIDQ769601
Publication date: 1958
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40)
Related Items (only showing first 100 items - show all)
Unnamed Item ⋮ Lax Theory Morphisms ⋮ Combinatory recursive objects of all finite types ⋮ Constructive Game Logic ⋮ Applications of type theory ⋮ Reductions of Residuals are Finite ⋮ (Head-)normalization of typeable rewrite systems ⋮ Explicit substitutions with de bruijn's levels ⋮ The combinator M and the Mockingbird lattice ⋮ Standard and Normal Reductions ⋮ Unnamed Item ⋮ Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach ⋮ Unnamed Item ⋮ Intersection and union types ⋮ Intuitive counterexamples for constructive fallacies ⋮ Combinatory categorial grammars as generators of weighted forests ⋮ Propositional forms of judgemental interpretations ⋮ Unnamed Item ⋮ Algebraic and Logical Operations on Operators One Application to Semantic Computation ⋮ Communicating contexts: A pragmatic approach to information exchange ⋮ Admissible ordering on monomials is well-founded: a constructive proof ⋮ An intensional formalization of generic statements ⋮ Paracompositionality, MWEs and argument substitution ⋮ Structural rules and algebraic properties of intersection types ⋮ Spiritus asper versus lambda: on the nature of functional abstraction ⋮ Classical realizability and arithmetical formulæ ⋮ Call-by-value combinatory logic and the lambda-value calculus ⋮ Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications ⋮ Structural Rules in Natural Deduction with Alternatives ⋮ λ-definierbare Funktionen auf Peanoalgebren ⋮ Point-fixe sur un ensemble restreint ⋮ Simplex sigillum veri: Peano, Frege, and Peirce on the Primitives of Logic ⋮ Three faces of natural deduction ⋮ Categories of First-Order Quantifiers ⋮ CARNAP’S DEFENSE OF IMPREDICATIVE DEFINITIONS ⋮ Realizability in ordered combinatory algebras with adjunction ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object ⋮ Type theoretic semantics for SemNet ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey ⋮ Unnamed Item ⋮ Approximation and normalization results for typeable term rewriting systems ⋮ The Cube Generalizing Aristotle’s Square in Logic of Determination of Objects (LDO) ⋮ Syntactic Type Soundness for the Region Calculus ⋮ Intersection Types and Computational Rules ⋮ Category theory based on combinatory logic ⋮ ASMs and Operational Algorithmic Completeness of Lambda Calculus ⋮ A CUCH-machine: The automatic treatment of bound variables ⋮ Some remarks about the connections between Combinatory Logic and axiomatic recursion theory ⋮ A glimpse into the paradise of combinatory algebra ⋮ Intuitionistic categorial grammar ⋮ Introduction to Type Theory ⋮ Mengentheoretische Modelle desλK-Kalküls ⋮ Unnamed Item ⋮ TYPED TIMED INPUT/OUTPUT AUTOMATA IN REAL-TIME, CYBERNETIC EXPLANATION ⋮ Why Sets? ⋮ First-Order Logic Without Bound Variables: Compositional Semantics ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Evolving combinators ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Encoding many-valued logic in $\lambda$-calculus ⋮ Unnamed Item ⋮ The Equivalence of Complete Reductions ⋮ Unnamed Item ⋮ Effective longest and infinite reduction paths in untyped λ-calculi ⋮ Proof-functional connectives and realizability ⋮ Non-well-founded sets via revision rules ⋮ An epistemic logic for becoming informed ⋮ From IF to BI. A tale of dependence and separation ⋮ Intersection types and lambda models ⋮ About probability-like measures for entire theories ⋮ Types for modules ⋮ OTTER experiments in a system of combinatory logic ⋮ Extracting a DPLL Algorithm ⋮ Combinatory logic with polymorphic types ⋮ Relevant predication. I: The formal theory ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ Finite generation and presentation problems for lambda calculus and combinatory logic ⋮ Combinatory logic and the semantics of substructural logics ⋮ Normal forms in combinatory logic ⋮ NP-completeness of a combinator optimization problem ⋮ A canonical locally named representation of binding ⋮ On explicit substitution with names ⋮ Polymorphic type inference and containment ⋮ Automath Type Inclusion in Barendregt’s Cube ⋮ Innovations in computational type theory using Nuprl ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ The word problem for Smullyan's lark combinator is decidable ⋮ Equivalence of bar recursors in the theory of functionals of finite type ⋮ A decidable theory of type assignment ⋮ A new type assignment for λ-terms ⋮ Type theory and concurrency ⋮ The ``relevance of intersection and union types ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ Intuitionistic completeness of first-order logic ⋮ Asymptotic Properties of Combinatory Logic
This page was built for publication: Combinatory logic. With two sections by William Craig.
