On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558): Difference between revisions

From MaRDI portal
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
(2 intermediate revisions by 2 users not shown)
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1016/0168-0072(88)90017-6 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W1527344590 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Recursion theoretic operators and morphisms on numbered sets / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3863873 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4068706 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Effectively given domains and lambda-calculus models / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4190093 / rank
 
Normal rank
Property / cites work
 
Property / cites work: \(\lambda\)-definability and recursiveness / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3708006 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Computability in higher types, P\(\omega\) and the completeness of type assignment / rank
 
Normal rank
Property / cites work
 
Property / cites work: The hereditary partial effective functionals and recursion theory in higher types / rank
 
Normal rank
Property / cites work
 
Property / cites work: Realizability and recursive set theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3335771 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3676137 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Data Types as Lattices / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3960746 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3959414 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3914974 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4029583 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3714051 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Categorical combinators / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3785893 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The system \({\mathcal F}\) of variable types, fifteen years later / rank
 
Normal rank
Property / cites work
 
Property / cites work: Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3671978 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Tripos theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Models of the lambda calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Deductive systems and categories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Functional completeness of cartesian categories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3342573 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3727946 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3677755 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Constructive natural deduction and its ‘ω-set’ interpretation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4145693 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4726252 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3659756 / rank
 
Normal rank
Property / cites work
 
Property / cites work: \(\mathbb{T}^\omega\) as a universal domain / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3216629 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Categories of partial maps / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5649639 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The „Dialectica”︁ Interpretation and Categories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Locally cartesian closed categories and type theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3768869 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Category-Theoretic Solution of Recursive Domain Equations / rank
 
Normal rank
Property / cites work
 
Property / cites work: Fixed-point constructions in order-enriched categories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Pre-adjunctions and lambda-algebraic theories / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3912779 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Resolution in type theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3922646 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A weak absolute consistency proof for some systems of illative combinatory logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Writing programs that construct proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3703866 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5625124 / rank
 
Normal rank
Property / cites work
 
Property / cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES / rank
 
Normal rank
Property / cites work
 
Property / cites work: Intuitionist type theory and the free topos / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4099613 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3328540 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3688389 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3343471 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3880323 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A sequent calculus formulation of type assignment with equality rules for the λβ-calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Combinators, \(\lambda\)-terms and proof theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Can programming be liberated from the von Neumann style? / rank
 
Normal rank
Property / cites work
 
Property / cites work: The lambda calculus. Its syntax and semantics. Rev. ed. / rank
 
Normal rank
Property / cites work
 
Property / cites work: A filter lambda model and the completeness of type assignment / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4160405 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Sequential algorithms on concrete data structures / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automatic synthesis of typed \(\Lambda\)-programs on term algebras / rank
 
Normal rank
Property / cites work
 
Property / cites work: Pebble, a kernel language for modules and abstract data types / rank
 
Normal rank
Property / cites work
 
Property / cites work: A set of postulates for the foundation of logic. II / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Type Theory of PL/CV3 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Completeness of type assignment in continuous lambda models / rank
 
Normal rank
Property / cites work
 
Property / cites work: A new type assignment for λ-terms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3221961 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3721820 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5686017 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Linear logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5573940 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Principal Type-Scheme of an Object in Combinatory Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Lambda‐Calculus Models and Extensionality / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4722037 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus / rank
 
Normal rank
Property / cites work
 
Property / cites work: Semantics-directed generation of a Prolog compiler / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4145861 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3216107 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A theory of type polymorphism in programming / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3705422 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Randomized geometric algorithms and pseudorandom generators / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4068054 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3677139 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3661543 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Intuitionistic propositional logic is polynomial-space complete / rank
 
Normal rank
Property / cites work
 
Property / cites work: Completeness, invariance and <i>λ</i>-definability / rank
 
Normal rank
Property / cites work
 
Property / cites work: Harvey Friedman's research on the foundations of mathematics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5183475 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard / rank
 
Normal rank
Property / cites work
 
Property / cites work: The L. E. J. Brouwer Centenary Symposium. Proceedings of the Conference held in Noordwijkerhout, 8--13 June, 1981 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus / rank
 
Normal rank

Latest revision as of 14:22, 19 June 2024

scientific article
Language Label Description Also known as
English
On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
scientific article

    Statements

    On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (English)
    0 references
    0 references
    1988
    0 references
    This is a survey paper whose central thesis is that Church's \(\lambda\)- calculus, rather than being one of many possible formalisms for computability theory, should be regarded as the core formal theory of computable functions and functionals. The author supports his main contention by surveying the principal connections between \(\lambda\)- calculus and three important areas in modern logic: higher type recursion theory, category theory, and proof theory. There are five sections in the paper and an extensive bibliography; the emphasis in each section is on structures invented for the semantics of typed and type-free \(\lambda\)- calculus.
    0 references
    survey
    0 references
    \(\lambda\)-calculus
    0 references
    higher type recursion theory
    0 references
    category theory
    0 references
    proof theory
    0 references
    bibliography
    0 references
    semantics
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references