Combinatory logic. Vol. II
From MaRDI portal
Publication:2553958
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)
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 (85)
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
This page was built for publication: Combinatory logic. Vol. II
