Combinatory logic. Vol. II

zbMath0242.02029MaRDI QIDQ2553958

Jonathan P. Seldin, J. Roger Hindley, Haskell B. Curry

Publication date: 1972

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

Mathematics Subject Classification ID

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

Typed equivalence, type assignment, and type containment, Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels, On the role of implication in formal logic, A characterization of F-complete type assignments, Reductions of Residuals are Finite, A combinatory account of internal structure, Annual meeting of the Association for Symbolic Logic, Anaheim, 1985, Formalizing non-termination of recursive programs, Combinatory logic with polymorphic types, Systems of illative combinatory logic complete for first-order propositional and predicate calculus, Directly reflective meta-programming, Standard and Normal Reductions, Some results on numerical systems in \(\lambda\)-calculus, Normal forms in combinatory logic, Bridging Curry and Church's typing style, NP-completeness of a combinator optimization problem, Unnamed Item, A decidable theory of type assignment, On adding (ξ) to weak equality in combinatory logic, A new type assignment for λ-terms, Principal type-schemes and condensed detachment, Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Unnamed Item, Curry's formalism as structuralism, An abstract Church-Rosser theorem. II: Applications, Meeting of the Association for Symbolic Logic, New York, 1971, The λ-calculus is ω-incomplete, Decreasing diagrams and relative termination, Unnamed Item, Efficiency of lambda-encodings in total type theory, Linear lambda terms as invariants of rooted trivalent maps, Correctness of compiling polymorphism to dynamic typing, Unnamed Item, How to assign ordinal numbers to combinatory terms with polymorphic types, A fuzzy language., The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction, Definierbare Funktionen imλ-Kalkül mit Typen, On the Unusual Effectiveness of Logic in Computer Science, The search for a reduction in combinatory logic equivalent to \(\lambda \beta\)-reduction. II., The Church-Rosser property in symmetric combinatory logic, Programming in the λ-Calculus: From Church to Scott and Back, Constructing type systems over an operational semantics, On the interpretation of combinators with weak reduction, Coquand's calculus of constructions: A mathematical foundation for a proof development system, Spaces with combinators, The Typed Böhm Theorem, On graph rewriting, reduction, and evaluation in the presence of cycles, New consecution calculi for \(R^{t}_{\to}\), Compact numeral representation with combinators, Principal types of BCK-lambda-terms, Category theory based on combinatory logic, New proofs of important theorems of untyped extensional \(\lambda\) calculus, A characterization of terms of the λI-calculus having a normal form, A weak absolute consistency proof for some systems of illative combinatory logic, Some remarks about the connections between Combinatory Logic and axiomatic recursion theory, A glimpse into the paradise of combinatory algebra, Intensional logic in extensional language, A sequent calculus for type assignment, Schönfinkel-type operators for classical logic, On the proof theory of Coquand's calculus of constructions, A direct proof of the confluence of combinatory strong reduction, 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08, A sequent calculus formulation of type assignment with equality rules for the λβ-calculus, A consistent combinatory logic with an inverse to equality, A solution to Curry and Hindley's problem on combinatory strong reduction, BUNDER’S PARADOX, The Church-Rosser property in dual combinatory logic, Expressive power of typed and type-free programming languages, Une nouvelle C\(\beta\)-réduction dans la logique combinatoire, Annual Meeting of the Association for Symbolic Logic, Washington, DC 1977, Sequential evaluation strategies for parallel-or and related reduction systems, Semantics for dual and symmetric combinatory calculi, Abstraction in Fitch's Basic Logic, A modern elaboration of the ramified theory of types, Equivalences between pure type systems and systems of illative combinatory logic, Curry's type-rules are complete with respect to the F-semantics too, The kernel strategy and its use for the study of combinatory logic, Barendregt's problem \#26 and combinatory strong reduction, Meeting of the Association for Symbolic Logic Florence, Italy 1982, Equality in, Redexes are stable in the λ-calculus, Types of I-free hereditary right maximal terms, The Equivalence of Complete Reductions, European Meeting of the Association for Symbolic Logic, Bristol, England, 1973