## Search results for 'Lambda calculus' (try it on Scholar)

1000+ found
Sort by:
1. H. P. Barendregt (1984). The Lambda Calculus: Its Syntax and Semantics. Sole Distributors for the U.S.A. And Canada, Elsevier Science Pub. Co..score: 90.0
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.

My bibliography

Export citation
2. Kazushige Terui (2007). Light Affine Lambda Calculus and Polynomial Time Strong Normalization. Archive for Mathematical Logic 46 (3-4):253-280.score: 90.0
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 (...)
No categories

My bibliography

Export citation
3. J. Roger Hindley (1986). Introduction to Combinators and [Lambda]-Calculus. Cambridge University Press.score: 87.0
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 (...)

My bibliography

Export citation
4. H. P. Barendregt (2013). Lambda Calculus with Types. Cambridge University Press.score: 75.0
This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.

My bibliography

Export citation
5. György E. Révész (1988). Lambda-Calculus, Combinators, and Functional Programming. Cambridge University Press.score: 75.0
No categories

My bibliography

Export citation
6. Henk Barendregt (1997). The Impact of the Lambda Calculus in Logic and Computer Science. Bulletin of Symbolic Logic 3 (2):181-215.score: 60.0
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.

My bibliography

Export citation
7. Kevin C. Klement (2003). Russell's 1903 - 1905 Anticipation of the Lambda Calculus. History and Philosophy of Logic 24 (1):15-37.score: 60.0
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 (...)

My bibliography

Export citation
8. Robert E. Byerly (1982). Recursion Theory and the Lambda-Calculus. Journal of Symbolic Logic 47 (1):67-83.score: 60.0
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.

My bibliography

Export citation
9. R. A. G. Seely (1987). Categorical Semantics for Higher Order Polymorphic Lambda Calculus. Journal of Symbolic Logic 52 (4):969-989.score: 60.0
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.

My bibliography

Export citation
10. Rainer Kerth (1998). The Interpretation of Unsolvable $Lambda$-Terms in Models of Untyped $Lambda$-Calculus. Journal of Symbolic Logic 63 (4):1529-1548.score: 60.0
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 (...)

My bibliography

Export citation
11. Yoriyuki Yamagata (2002). Strong Normalization of a Symmetric Lambda Calculus for Second-Order Classical Logic. Archive for Mathematical Logic 41 (1):91-99.score: 60.0
We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its strong normalization.
No categories

My bibliography

Export citation
12. Chris Hankin (1994). Lambda Calculi: A Guide for the Perplexed. Oxford University Press.score: 54.0
The lambda-calculus lies at the very foundation of computer science. Besides its historical role in computability theory it has had significant influence on programming language design and implementation, denotational semantics and domain theory. The book emphasizes the proof theory for the type-free lambda-calculus. The first six chapters concern this calculus and cover the basic theory, reduction, models, computability, and the relationship between the lambda-calculus and combinatory logic. Chapter 7 presents a variety of typed (...)
No categories

My bibliography

Export citation
13. Sachio Hirokawa (1992). The Converse Principal Type-Scheme Theorem in Lambda Calculus. Studia Logica 51 (1):83 - 95.score: 48.0
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 (...)

My bibliography

Export citation
14. Benedetto Intrigila (1994). Some Results on Numeral Systems in $\Lambda$ -Calculus. Notre Dame Journal of Formal Logic 35 (4):523-541.score: 48.0
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 (...)

My bibliography

Export citation
15. René David & Karim Nour (1995). Storage Operators and Directed Lambda-Calculus. Journal of Symbolic Logic 60 (4):1054-1086.score: 48.0
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 (...)

My bibliography

Export citation
16. Jean-Louis Krivine (2001). Typed Lambda-Calculus in Classical Zermelo-Frænkel Set Theory. Archive for Mathematical Logic 40 (3):189-205.score: 48.0
, 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, (...)
No categories

My bibliography

Export citation
17. score: 45.0
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof (...)

My bibliography

Export citation
18. M. Coppo & M. Dezani-Ciancaglini (1980). An Extension of the Basic Functionality Theory for the $\Lambda$-Calculus. Notre Dame Journal of Formal Logic 21 (4):685-693.score: 45.0

My bibliography

Export citation
19. Simona Ronchi della Rocca & Luca Roversi (1997). Lambda Calculus and Intuitionistic Linear Logic. Studia Logica 59 (3):417-448.score: 45.0
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.

My bibliography

Export citation
20. David D. McDonald (1994). 'Krisp': A Represnetation for the Semantic Interpretation of Texts. [REVIEW] Minds and Machines 4 (1):59-73.score: 45.0
KRISP is a representation system and set of interpretation protocols that is used in the Sparser natural language understanding system to embody the meaning of texts and their pragmatic contexts. It is based on a denotational notion of semantic interpretation, where the phrases of a text are directly projected onto a largely pre-existing set of individuals and categories in a model, rather than first going through a level of symbolic representation such as a logical form. It defines a small set (...)

My bibliography

Export citation
21. Harold Simmons (2000). Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge University Press.score: 45.0
Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied (...)

My bibliography

Export citation
22. Simona Ronchi Della Rocca & Luca Roversi (1997). Lambda Calculus and Intuitionistic Linear Logic. Studia Logica 59 (3):417-448.score: 45.0
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.

My bibliography

Export citation
23. Harold T. Hodes (1988). Book Review. The Lambda-Calculus. H. P. Barendregt(. [REVIEW] Philosophical Review 97 (1):132-7.score: 45.0
Translate to English

My bibliography

Export citation
24. Bruce Lercher (1976). Lambda-Calculus Terms That Reduce to Themselves. Notre Dame Journal of Formal Logic 17 (2):291-292.score: 45.0

My bibliography

Export citation
25. Garrel Pottinger (1981). The Church-Rosser Theorem for the Typed $\Lambda$-Calculus with Surjective Pairing. Notre Dame Journal of Formal Logic 22 (3):264-268.score: 45.0

My bibliography

Export citation
26. M. W. Bunder (1979). Variable Binding Term Operators in $\Lambda$-Calculus. Notre Dame Journal of Formal Logic 20 (4):876-878.score: 45.0

My bibliography

Export citation
27. score: 45.0
No categories

My bibliography

Export citation
28. score: 45.0

My bibliography

Export citation
29. E. Engeler (1984). Review: H. P. Barendregt, The Lambda Calculus. Its Syntax and Semantics. [REVIEW] Journal of Symbolic Logic 49 (1):301-303.score: 45.0

My bibliography

Export citation
30. Garrel Pottinger (1978). Proofs of the Normalization and Church-Rosser Theorems for the Typed $\Lambda$-Calculus. Notre Dame Journal of Formal Logic 19 (3):445-451.score: 45.0

My bibliography

Export citation
31. R. Hindley & G. Longo (1980). LambdaCalculus Models and Extensionality. Mathematical Logic Quarterly 26 (19‐21):289-310.score: 45.0
No categories

My bibliography

Export citation
32. J. L. Krivine (1988). Review: J. Roger Hindley, Jonathan P. Seldin, Introduction to Combinators and $Lambda$-Calculus. [REVIEW] Journal of Symbolic Logic 53 (3):985-986.score: 45.0

My bibliography

Export citation
33. Giuseppe Longo (1987). Review: C. P. J. Koymans, Models of the Lambda Calculus. [REVIEW] Journal of Symbolic Logic 52 (1):284-285.score: 45.0

My bibliography

Export citation
34. G. D. Plotkin (1974). The $Lambda$-Calculus is $Omega$-Incomplete. Journal of Symbolic Logic 39 (2):313-317.score: 45.0

My bibliography

Export citation
35. Luis E. Sanchis (1987). Completeness of Transfinite Evaluation in an Extension of the Lambda Calculus. Journal of Symbolic Logic 52 (1):243-275.score: 45.0

My bibliography

Export citation
36. score: 45.0

My bibliography

Export citation
37. Silvio Valentini (2001). An Elementary Proof of Strong Normalization for Intersection Types. Archive for Mathematical Logic 40 (7):475-488.score: 45.0
We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly (...)
No categories

My bibliography

Export citation
38. Roberto M. Amadio (1998). Domains and Lambda-Calculi. Cambridge University Press.score: 42.0
This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way, and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological (...)
No categories

My bibliography

Export citation
39. Michael Gabbay (2011). A Proof-Theoretic Treatment of Λ-Reduction with Cut-Elimination: Λ-Calculus as a Logic Programming Language. Journal of Symbolic Logic 76 (2):673 - 699.score: 42.0
We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

My bibliography

Export citation
40. Motohiko Mouri & Norihiro Kamide (2008). Strong Normalizability of Typed Lambda-Calculi for Substructural Logics. Logica Universalis 2 (2):189-207.score: 39.0
The strong normalization theorem is uniformly proved for typed λ-calculi for a wide range of substructural logics with or without strong negation.

My bibliography

Export citation
41. Pierluigi Minari (2007). Analytic Proof Systems for Λ-Calculus: The Elimination of Transitivity, and Why It Matters. [REVIEW] Archive for Mathematical Logic 46 (5-6):385-424.score: 39.0
We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free derivations—of a number (...)
No categories

My bibliography

Export citation
42. Silvio Valentini (1992). The Judgement Calculus for Intuitionistic Linear Logic: Proof Theory and Semantics. Mathematical Logic Quarterly 38 (1):39-58.score: 39.0
No categories

My bibliography

Export citation
43. Henk Barendregt (1973). A Characterization of Terms of the |Lambda I-Calculus Having a Normal Form. Journal of Symbolic Logic 38 (3):441 - 445.score: 36.0

My bibliography

Export citation
44. Michael Moortgat (2009). Symmetric Categorial Grammar. Journal of Philosophical Logic 38 (6):681 - 710.score: 33.0
The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of natural (...)

My bibliography

Export citation
45. Fairouz Kamareddine & Ewan Klein (1993). Nominalization, Predication and Type Containment. Journal of Logic, Language and Information 2 (3):171-215.score: 33.0
In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements are contained (...)

My bibliography

Export citation
46. Jonathan P. Seldin (2000). On the Role of Implication in Formal Logic. Journal of Symbolic Logic 65 (3):1076-1114.score: 33.0
Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λ-calculus with logical constants for and, or, all, and exists, but with none for either implication or negation. The proof is strictly finitary, showing that this system is very weak. The results can be extended to a "classical" version of the system. They (...)

My bibliography

Export citation
47. score: 33.0
This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.

My bibliography

Export citation
48. William R. Stirton (2013). A Decidable Theory of Type Assignment. Archive for Mathematical Logic 52 (5-6):631-658.score: 33.0
This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard’s F (Proofs and types. Cambridge University Press, Cambridge, 1989). It is like the simple theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recursive (...)
No categories

My bibliography

Export citation
49. score: 30.0
This text is a short introduction to logic that was primarily used for accompanying an introductory course in Logic for Linguists held at the New University of Lisbon (UNL) in fall 2010. The main idea of this course was to give students the formal background and skills in order to later assess literature in logic, semantics, and related fields and perhaps even use logic on their own for the purpose of doing truth-conditional semantics. This course in logic does not replace (...)
Translate to English