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
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, Revisiting the notion of function, Logic of determination of objects (LDO): how to articulate ``extension with ``intension and ``objects with ``concepts, Curry's formalism as structuralism, On the Logic of Expansion in Natural Language, Second-order properties of undirected graphs, Do-it-yourself type theory, How to assign ordinal numbers to combinatory terms with polymorphic types, On a machine-checked proof for fraction arithmetic over a GCD domain, The semantics of entailment omega, The heart of intersection type assignment: Normalisation proofs revisited, Composition of deductions within the propositions-as-types paradigm, Condensed detachment is complete for relevance logic: A computer-aided proof, Objectivity and Truth in Mathematics: A Sober Non-platonist Perspective, Term-space semantics of typed lambda calculus, State-transition machines for lambda-calculus expressions, Krivine Machines and Higher-Order Schemes, Covert Movement in Logical Grammar, Type-theoretic logic with an operational account of intensionality, A logical analysis of the Anselm's \textit{Unum argumentum} (from \textit{Proslogion}), Coquand's calculus of constructions: A mathematical foundation for a proof development system, Spaces with combinators, The systematic construction of a one-combinator basis for lambda-terms, Monadic pseudo BCI-algebras and corresponding logics, Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment, AI, ME and Lewis (abelian implication, material equivalence and C I Lewis 1920), Principal types of BCK-lambda-terms, A verified framework for higher-order uncurrying optimizations, New proofs of important theorems of untyped extensional \(\lambda\) calculus, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Combinator operations, Logic of subtyping, Proof-theoretic semantics for classical mathematics, Completeness of the normal typed fragment of the \(\lambda\)-system \(U\), A new way of normalizing intuitionistic propositional logic, Implementing a computer algebra system in Haskell, Schönfinkel-type operators for classical logic, The harmony of identity, Synchronization and computing capabilities of linear asynchronous structures, The \(\lambda \)-calculus and the unity of structural proof theory, Positive logic and \(\lambda\)-constants, A new theory of quantifiers and term connectives, Some models of combinatory logic, A solution to Curry and Hindley's problem on combinatory strong reduction, Algorithmic reduction of biological networks with multiple time scales, The tree-generative capacity of combinatory categorial grammars, About systems of equations, X-separability, and left-invertibility in the \(\lambda\)-calculus, Logic of typical and atypical instances of a concept -- a mathematical model, Type inference with recursive types: Syntax and semantics, The lambda-gamma calculus: A language adequate for defining recursive functions, Une nouvelle C\(\beta\)-réduction dans la logique combinatoire, Semantics for dual and symmetric combinatory calculi, Generalized filter models, A Gentzen-style sequent calculus of constructions with expansion rules, On the semantics of polymorphism, A modern elaboration of the ramified theory of types, Linear numeral systems, On principal types of combinators, Normalization, approximation, and semantics for combinator systems, Syntactic type soundness results for the region calculus, Conservation and uniform normalization in lambda calculi with erasing reductions, Propositions and specifications of programs in Martin-Löf's type theory, The absence and the presence of fixed point combinators, Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result, A variadic extension of Curry's fixed-point combinator, Types of I-free hereditary right maximal terms, Why ramify?, Constructive mathematics, Church's thesis, and free choice sequences, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, The future of logic: foundation-independence
