Switch to: Citations

References in:

Typed lambda calculus

In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132 (1977)

Add references

You must login to add references.
  1. Combinatory Logic.J. Barkley Rosser - 1967 - Journal of Symbolic Logic 32 (2):267-268.
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Handbook of Logic in Computer Science.S. Abramsky, D. Gabbay & T. Maibaurn (eds.) - 1992 - Oxford University Press.
    Translate
     
     
    Export citation  
     
    Bookmark   10 citations  
  • Combinatory Logic.Haskell B. Curry - 1958 - Amsterdam: North-Holland Pub. Co..
    CHAPTER Addenda to Pure Combinatory Logic This chapter will treat various additions to, and modifications of, the subject matter of Chapters-7. ...
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   75 citations  
  • Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Stockholm, Sweden: Dover Publications.
    This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   311 citations  
  • Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Mathematical Logic Quarterly 27 (2‐6):45-58.
  • Pairing Without Conventional Restraints.Henk Barendregt - 1974 - Mathematical Logic Quarterly 20 (19‐22):289-306.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Pairing Without Conventional Restraints.Henk Barendregt - 1974 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 20 (19-22):289-306.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Functional Characters of Solvable Terms.M. Coppo, M. Dezani-Ciancaglini & B. Venneri - 1981 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 27 (2-6):45-58.
    Direct download  
     
    Export citation  
     
    Bookmark   9 citations  
  • An Unsolvable Problem of Elementary Number Theory.Alonzo Church - 1936 - Journal of Symbolic Logic 1 (2):73-74.
  • Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1.
  • The Formulae-as-Types Notion of Construction.William Alvin Howard - 1980 - In Haskell Curry, Hindley B., Seldin J. Roger & P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press.
    No categories
     
    Export citation  
     
    Bookmark   89 citations  
  • Equivalence of Bar Recursors in the Theory of Functionals of Finite Type.Marc Bezem - 1988 - Archive for Mathematical Logic 27 (2):149-160.
    The main result of this paper is the equivalence of several definition schemas of bar recursion occurring in the literature on functionals of finite type. We present the theory of functionals of finite type, in [T] denoted byqf-WE-HA ω, which is necessary for giving the equivalence proofs. Moreover we prove two results on this theory that cannot be found in the literature, namely the deduction theorem and a derivation of Spector's rule of extensionality from [S]: ifP→T 1=T 2 and Q[X∶≡T1], (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • A Formulation of the Simple Theory of Types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
  • Higher Order Matching is Undecidable.Ralph Loader - 2003 - Logic Journal of the IGPL 11 (1):51-68.
    We show that the solvability of matching problems in the simply typed λ-calculus, up to β equivalence, is not decidable. This decidability question was raised by Huet [4].Note that there are two variants of the question: that concerning β equivalence, and that concerning βη equivalence.The second of these is perhaps more interesting; unfortunately the work below sheds no light on it, except perhaps to illustrate the subtlety and difficulty of the problem.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On Definition Trees of Ordinal Recursive Functonals: Reduction of the Recursion Orders by Means of Type Level Raising.Jan Terlouw - 1982 - Journal of Symbolic Logic 47 (2):395-402.
  • Completeness, Invariance and Λ-Definability.R. Statman - 1982 - Journal of Symbolic Logic 47 (1):17-26.
  • Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus.Henk Barendregt, Martin Bunder & Wil Dekkers - 1993 - Journal of Symbolic Logic 58 (3):769-788.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • The Emptiness Problem for Intersection Types.Paweł Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.
    We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  • Third Order Matching is Decidable.Gilles Dowek - 1994 - Annals of Pure and Applied Logic 69 (2-3):135-155.
    The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed [lgr]-calculus, i.e. to solve the equation a = b where a and b are simply typed [lgr]-terms and b is ground. The decidability of this problem is still open. We prove the decidability of the particular case in which the variables occuring in the problem are at most third order.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Domain Theory in Logical Form.Samson Abramsky - 1991 - Annals of Pure and Applied Logic 51 (1-2):1-77.
    Abramsky, S., Domain theory in logical form, Annals of Pure and Applied Logic 51 1–77. The mathematical framework of Stone duality is used to synthesise a number of hitherto separate developments in theoretical computer science.• Domain theory, the mathematical theory of computation introduced by Scott as a foundation for detonational semantics• The theory of concurrency and systems behaviour developed by Milner, Hennesy based on operational semantics.• Logics of programsStone duality provides a junction between semantics and logics . Moreover, the underlying (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  • Λ-Definability on Free Algebras.Marek Zaionc - 1991 - Annals of Pure and Applied Logic 51 (3):279-300.
    Zaionc, M., λ-Definability on free algebras, Annals of Pure and Applied Logic 51 279-300. A λ-language over a simple type structure is considered. There is a natural isomorphism which identifies free algebras with nonempty second-order types. If A is a free algebra determined by the signature SA = [α1,...,αn], then by a type τA we mean τ1,...,τn→0 where τi=0αi→0. It can be seen that closed terms of the type τA reflex constructions in the algebra A. Therefore any term of the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • On Church's Formal Theory of Functions and Functionals.Giuseppe Longo - 1988 - Annals of Pure and Applied Logic 40 (2):93-133.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Decision Problem for Exponential Diophantine Equations.Martin Davis, Hilary Putnam & Julia Robinson - 1970 - Journal of Symbolic Logic 35 (1):151-152.
  • The Emptiness Problem for Intersection Types.Pawel Urzyczyn - 1999 - Journal of Symbolic Logic 64 (3):1195-1215.
    We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system we show that the emptiness problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable.
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Universal Diophantine Equation.James P. Jones - 1982 - Journal of Symbolic Logic 47 (3):549-571.
  • Completeness of the Propositions-as-Types Interpretation of Intuitionistic Logic Into Illative Combinatory Logic.Wil Dekkers, Martin Bunder & Henk Barendregt - 1998 - Journal of Symbolic Logic 63 (3):869-890.
    Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Interpretation of Analysis by Means of Constructive Functionals of Finite Types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in Mathematics. Amsterdam: North-Holland Pub. Co.. pp. 101--128.
     
    Export citation  
     
    Bookmark   54 citations  
  • A Filter Lambda Model and the Completeness of Type Assignment.Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini - 1983 - Journal of Symbolic Logic 48 (4):931-940.
  • Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.N. G. De Bruijn - 1975 - Journal of Symbolic Logic 40 (3):470-470.
    Direct download  
     
    Export citation  
     
    Bookmark   15 citations