Categorical combinators
From MaRDI portal
Publication:3745827
DOI10.1016/S0019-9958(86)80047-XzbMath0607.03005OpenAlexW2912512531MaRDI QIDQ3745827
Publication date: 1986
Published in: Information and Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0019-9958(86)80047-x
Cartesian closed categoriesfunctional programminglambda-calculussurjective pairingcategorical combinatory logic
Abstract data types; algebraic specification (68Q65) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40) Foundations, relations to logic and deductive systems (18A15)
Related Items
Simply typed lambda calculus with first-class environments, Functional programming with combinators, Church-Rosser theorem for a rewriting system on categorical combinators, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, A notation for lambda terms. A generalization of environments, A formal logic for formal category theory, A category-theoretic characterization of functional completeness, Alpha conversion, conditions on variables and categorical logic, Reverse AD at higher types: pure, principled and denotationally correct, Quasi-prime algebraic domains, A formalized general theory of syntax with bindings: extended version, Semantics of the typed \(\lambda\)-calculus with substitution in a cartesian closed category, A proof of the substitution lemma in de Bruijn's notation, Unnamed Item, Unnamed Item, λν, a calculus of explicit substitutions which preserves strong normalisation, Categories with Families: Unityped, Simply Typed, and Dependently Typed
