Results for 'Lambda calculus'

1000+ found
Order:
  1.  70
    The Lambda Calculus: Its Syntax and Semantics.H. P. Barendregt - 1984 - Elsevier.
    The revised edition contains a new chapter which provides an elegant description of the semantics. The various classes of lambda calculus models are described in a uniform manner. Some didactical improvements have been made to this edition. An example of a simple model is given and then the general theory (of categorical models) is developed. Indications are given of those parts of the book which can be used to form a coherent course.
    Direct download  
     
    Export citation  
     
    My bibliography   50 citations  
  2.  53
    Strong Normalization of a Symmetric Lambda Calculus for Second-Order Classical Logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.
    We extend Barbanera and Berardi’s symmetric lambda calculus to second order classical propositional logic and prove its strong normalization.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  3.  30
    Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
    Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, we (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  4.  25
    Introduction to Combinators and [Lambda]-Calculus.J. Roger Hindley - 1986 - Cambridge University Press.
    Combinatory logic and lambda-conversion were originally devised in the 1920s for investigating the foundations of mathematics using the basic concept of 'operation' instead of 'set'. They have now developed into linguistic tools, useful in several branches of logic and computer science, especially in the study of programming languages. These notes form a simple introduction to the two topics, suitable for a reader who has no previous knowledge of combinatory logic, but has taken an undergraduate course in predicate calculus (...)
    Direct download  
     
    Export citation  
     
    My bibliography   11 citations  
  5.  14
    Lambda Calculus with Types.H. P. Barendregt - 2013 - Cambridge University Press.
    This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  6. Lambda-Calculus, Combinators, and Functional Programming.György E. Révész - 1988 - Cambridge University Press.
  7.  40
    Russell's 1903 - 1905 Anticipation of the Lambda Calculus.Kevin C. Klement - 2003 - History and Philosophy of Logic 24 (1):15-37.
    Philosophy Dept, Univ. of Massachusetts, 352 Bartlett Hall, 130 Hicks Way, Amherst, MA 01003, USA Received 22 July 2002 It is well known that the circumflex notation used by Russell and Whitehead to form complex function names in Principia Mathematica played a role in inspiring Alonzo Church’s ‘Lambda Calculus’ for functional logic developed in the 1920s and 1930s. Interestingly, earlier unpublished manuscripts written by Russell between 1903 and 1905—surely unknown to Church—contain a more extensive anticipation of the essential (...)
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  8.  13
    Categorical Semantics for Higher Order Polymorphic Lambda Calculus.R. A. G. Seely - 1987 - Journal of Symbolic Logic 52 (4):969-989.
    A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including "subtypes", for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  9.  69
    The Impact of the Lambda Calculus in Logic and Computer Science.Henk Barendregt - 1997 - Bulletin of Symbolic Logic 3 (2):181-215.
    One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  10.  8
    Inductive Types and Type Constraints in the Second-Order Lambda Calculus.Nax Paul Mendler - 1991 - Annals of Pure and Applied Logic 51 (1-2):159-172.
    Mendler, N.P., Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic 51 159–172. We add to the second-order lambda calculus the type constructors μ and ν, which give the least and greatest solutions to positively defined type expressions. Strong normalizability of typed terms is shown using Girard's candidat de réductibilité method. Using the same structure built for that proof, we prove a necessary and sufficient condition for determining when a (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  11.  27
    1. Intuitionistic Sentential Calculus with Iden-Tity.Intuitionistic Sentential Calculus - 1990 - Bulletin of the Section of Logic 19 (3):92-99.
  12.  3
    Kripke-Style Models for Typed Lambda Calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
    Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  13.  24
    Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
    The [lambda]-calculus can be represented topologically by assigning certain spaces to the types and certain continuous maps to the terms. Using a recent result from category theory, the usual calculus of [lambda]-conversion is shown to be deductively complete with respect to such topological semantics. It is also shown to be functionally complete, in the sense that there is always a ‘minimal’ topological model in which every continuous function is [lambda]-definable. These results subsume earlier ones using (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  14.  5
    Ordinals and Ordinal Functions Representable in the Simply Typed Lambda Calculus.N. Danner - 1999 - Annals of Pure and Applied Logic 97 (1-3):179-201.
    We define ordinal representations in the simply typed lambda calculus, and consider the ordinal functions representable with respect to these notations. The results of this paper have the same flavor as those of Schwichtenberg and Statman on numeric functions representable in the simply typed lambda calculus. We define four families of ordinal notations; in order of increasing generality of the type of notation, the representable functions consist of the closure under composition of successor and α ωα, (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  15.  13
    Recursion Theory and the Lambda-Calculus.Robert E. Byerly - 1982 - Journal of Symbolic Logic 47 (1):67-83.
    A semantics for the lambda-calculus due to Friedman is used to describe a large and natural class of categorical recursion-theoretic notions. It is shown that if e 1 and e 2 are godel numbers for partial recursive functions in two standard ω-URS's 1 which both act like the same closed lambda-term, then there is an isomorphism of the two ω-URS's which carries e 1 to e 2.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  16.  3
    The Interpretation of Unsolvable $Lambda$-Terms in Models of Untyped $Lambda$-Calculus.Rainer Kerth - 1998 - Journal of Symbolic Logic 63 (4):1529-1548.
    Our goal in this paper is to analyze the interpretation of arbitrary unsolvable $\lambda$-terms in a given model of $\lambda$-calculus. We focus on graph models and (a special type of) stable models. We introduce the syntactical notion of a decoration and the semantical notion of a critical sequence. We conjecture that any unsolvable term $\beta$-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those two notions: given a graph model (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  17.  1
    Skew Confluence and the Lambda Calculus with Letrec.Zena M. Ariola & Stefan Blom - 2002 - Annals of Pure and Applied Logic 117 (1-3):95-168.
    We present an extension of the lambda calculus with the letrec construct. In contrast to current theories, which impose restrictions on where the rewriting can take place, our theory is very liberal, e.g., it allows rewriting under lambda abstractions and on cycles. As shown previously, the reduction theory is non-confluent. Thus, we searched for and found a new property that resembles confluence and that is equivalent to uniqueness of infinite normal forms: skew confluence. This notion is based (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  18.  4
    Reduction Rules for Intuitionistic {{Lambda}{Rho}}-Calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
    The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  19.  14
    Typed Lambda-Calculus in Classical Zermelo-Frænkel Set Theory.Jean-Louis Krivine - 2001 - Archive for Mathematical Logic 40 (3):189-205.
    , which uses the intuitionistic propositional calculus, with the only connective →. It is very important, because the well known Curry-Howard correspondence between proofs and programs was originally discovered with it, and because it enjoys the normalization property: every typed term is strongly normalizable. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F, still with the normalization property.More recently, in 1990, the Curry-Howard correspondence was extended to classical logic, (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  20.  40
    Storage Operators and Directed Lambda-Calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
    Storage operators have been introduced by J. L. Krivine in [5] they are closed λ-terms which, for a data type, allow one to simulate a "call by value" while using the "call by name" strategy. In this paper, we introduce the directed λ-calculus and show that it has the usual properties of the ordinary λ-calculus. With this calculus we get an equivalent--and simple--definition of the storage operators that allows to show some of their properties: $\bullet$ the stability (...)
    Direct download (9 more)  
     
    Export citation  
     
    My bibliography  
  21.  3
    Continuous Normalization for the Lambda-Calculus and Gödel’s T.Klaus Aehlig & Felix Joachimski - 2005 - Annals of Pure and Applied Logic 133 (1-3):39-71.
    Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  22.  11
    The Converse Principal Type-Scheme Theorem in Lambda Calculus.Sachio Hirokawa - 1992 - Studia Logica 51 (1):83 - 95.
    A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  23.  4
    Some Results on Numeral Systems in $\Lambda$ -Calculus.Benedetto Intrigila - 1994 - Notre Dame Journal of Formal Logic 35 (4):523-541.
    In this paper we study numeral systems in the -calculus. With one exception, we assume that all numerals have normal form. We study the independence of the conditions of adequacy of numeral systems. We find that, to a great extent, they are mutually independent. We then consider particular examples of numeral systems, some of which display paradoxical properties. One of these systems furnishes a counterexample to a conjecture of Böhm. Next, we turn to the approach of Curry, Hindley, and (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  24. Substructural Logics, Combinatory Logic, and Lambda-Calculus.Katalin Bimbo - 1999 - Dissertation, Indiana University
    The dissertation deals with problems in "logic", more precisely, it deals with particular formal systems aiming at capturing patterns of valid reasoning. Sequent calculi were proposed to characterize logical connectives via introduction rules. These systems customarily also have structural rules which allow one to rearrange the set of premises and conclusions. In the "structurally free logic" of Dunn and Meyer the structural rules are replaced by combinatory rules which allow the same reshuffling of formulae, and additionally introduce an explicit marker (...)
     
    Export citation  
     
    My bibliography  
  25.  6
    Classical Logic, Storage Operators and Second-Order Lambda-Calculus.Jean-Louis Krivine - 1994 - Annals of Pure and Applied Logic 68 (1):53-78.
    We describe here a simple method in order to obtain programs from proofs in second-order classical logic. Then we extend to classical logic the results about storage operators proved by Krivine for intuitionistic logic. This work generalizes previous results of Parigot.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   6 citations  
  26.  16
    Lambda-Calculus Models and Extensionality.R. Hindley & G. Longo - 1980 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 26 (19-21):289-310.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  27.  1
    The |Lambda-Calculus.H. P. Barendregt - 1988 - Philosophical Review 97 (1):132-137.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  28.  9
    Lambda-Calculus and Combinators in the 20th Century.Felice Cardone & J. Roger Hindley - 2009 - In Dov Gabbay (ed.), The Handbook of the History of Logic. Elsevier. pp. 5--723.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  29.  9
    An Extension of the Basic Functionality Theory for the $\Lambda$-Calculus.M. Coppo & M. Dezani-Ciancaglini - 1980 - Notre Dame Journal of Formal Logic 21 (4):685-693.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  30.  31
    Proof Nets and the Lambda-Calculus.Stefano Guerrini - 2004 - In Thomas Ehrhard (ed.), Linear Logic in Computer Science. Cambridge University Press. pp. 316--65.
    Direct download  
     
    Export citation  
     
    My bibliography  
  31.  10
    LambdaCalculus Models and Extensionality.R. Hindley & G. Longo - 1980 - Mathematical Logic Quarterly 26 (19‐21):289-310.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  32.  11
    Typed Lambda Calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 1091--1132.
    Direct download  
     
    Export citation  
     
    My bibliography   4 citations  
  33. Some Results on Extensionality in Lambda Calculus.Benedetto Intrigila & Richard Statman - 2005 - Annals of Pure and Applied Logic 132 (2-3):109-125.
    In this paper we consider the problem of the existence of a λ-theory T such that:–T is recursive enumerable;–the ω-rule holds in T .We solve affirmatively this problem.Some related questions are also discussed.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  34. Set-Theoretical Models of Lambda-Calculus: Theories, Expansions, Isomorphisms.G. Longo - 1983 - Annals of Pure and Applied Logic 24 (2):153.
    Direct download  
     
    Export citation  
     
    My bibliography   2 citations  
  35.  3
    Completeness of Transfinite Evaluation in an Extension of the Lambda Calculus.Luis E. Sanchis - 1987 - Journal of Symbolic Logic 52 (1):243-275.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  36.  3
    A Tour of the Multivariate Lambda Calculus.Garrel Pottinger - 1990 - In J. Dunn & A. Gupta (eds.), Truth or Consequences. Kluwer Academic Publishers. pp. 209--229.
    Direct download  
     
    Export citation  
     
    My bibliography   1 citation  
  37.  12
    Strong Normalization of Program-Indexed Lambda Calculus.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (1/2):65-78.
    Direct download  
     
    Export citation  
     
    My bibliography  
  38.  14
    Book Review. The Lambda-Calculus. H. P. Barendregt(. [REVIEW]Harold T. Hodes - 1988 - Philosophical Review 97 (1):132-7.
    Translate
      Direct download  
     
    Export citation  
     
    My bibliography  
  39.  6
    Variable Binding Term Operators in $\Lambda $-Calculus.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (4):876-878.
  40.  3
    Proofs of the Normalization and Church-Rosser Theorems for the Typed $\Lambda$-Calculus.Garrel Pottinger - 1978 - Notre Dame Journal of Formal Logic 19 (3):445-451.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  41.  23
    Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.This paper introduces a typed functional language ! and a categorical model for it.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  42. Review: C. P. J. Koymans, Models of the Lambda Calculus[REVIEW]Giuseppe Longo - 1987 - Journal of Symbolic Logic 52 (1):284-285.
     
    Export citation  
     
    My bibliography  
  43.  13
    Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  44.  5
    Monads and Meta-Lambda Calculus.Daisuke Bekki - 2009 - In Hattori (ed.), New Frontiers in Artificial Intelligence. Springer. pp. 193--208.
    Direct download  
     
    Export citation  
     
    My bibliography  
  45.  2
    Barendregt H. P.. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and Foundations of Mathematics, Vol. 103. North-Holland Publishing Company, Amsterdam, New York, and Oxford, 1981, Xiv + 615 Pp. [REVIEW]E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  46.  2
    Book Review: Henk Barendregt, Will Dekkers, Richard Statman Et Al., Lambda Calculus With Types. [REVIEW]Adrian Rezuş - 2015 - Studia Logica 103 (6):1319-1326.
  47.  2
    The $Lambda$-Calculus is $Omega$-Incomplete.G. D. Plotkin - 1974 - Journal of Symbolic Logic 39 (2):313-317.
  48.  2
    Review: J. Roger Hindley, Jonathan P. Seldin, Introduction to Combinators and $Lambda$-Calculus[REVIEW]J. L. Krivine - 1988 - Journal of Symbolic Logic 53 (3):985-986.
  49.  3
    The Church-Rosser Theorem for the Typed $\Lambda$-Calculus with Surjective Pairing.Garrel Pottinger - 1981 - Notre Dame Journal of Formal Logic 22 (3):264-268.
  50.  2
    Lambda-Calculus Terms That Reduce to Themselves.Bruce Lercher - 1976 - Notre Dame Journal of Formal Logic 17 (2):291-292.
1 — 50 / 1000