Results for 'Typed λ-calculus'

927 found
Order:
  1. A typed λ-calculus and Girard's model of ptykes.Peter Päppinghaus - 1985 - In G. Dorn & P. Weingarten, Foundations of Logic and Linguistics. Problems and Solutions. Plenum. pp. 245--279.
    No categories
     
    Export citation  
     
    Bookmark  
  2.  61
    (1 other version)A Gentzen-type calculus of sequents for single-operator propositional logic.John Riser - 1967 - Journal of Symbolic Logic 32 (1):75-80.
  3.  90
    Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T.Felix Joachimski & Ralph Matthes - 2003 - Archive for Mathematical Logic 42 (1):59-87.
    Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed λ-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   19 citations  
  4.  94
    Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
    We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ-calculus with β-, ξ- and η-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  5.  54
    John Riser. A Gentzen-type calculus of sequents for single-operator propositional logic. The Journal of symbolic logic, vol. 32 , pp. 75–80. [REVIEW]Gene F. Rose - 1968 - Journal of Symbolic Logic 33 (1):129-129.
  6.  75
    An upper bound for reduction sequences in the typed λ-calculus.Helmut Schwichtenberg - 1991 - Archive for Mathematical Logic 30 (5-6):405-408.
  7.  36
    A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
    In this paper, we define a realizability semantics for the simply typed $lambdamu$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  62
    Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
    The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  9. 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  10.  44
    Lambda calculus with types.H. P. Barendregt - 2013 - New York: Cambridge University Press. Edited by Wil Dekkers & Richard Statman.
    This handbook with exercises reveals the mathematical beauty of formalisms hitherto mostly used for software and hardware design and verification.
    Direct download  
     
    Export citation  
     
    Bookmark   7 citations  
  11.  20
    A Multi-type Display Calculus for Dynamic Epistemic Logic.Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano & Vlasta Sikimić - 2016 - Journal of Logic and Computation 6 (26):2017–2065.
    In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic (...)
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  12.  30
    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 collection (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  13.  19
    Bell-Type Inequalities from the Perspective of Non-Newtonian Calculus.Michał Piotr Piłat - 2024 - Foundations of Science 29 (2):441-457.
    A class of quantum probabilities is reformulated in terms of non-Newtonian calculus and projective arithmetic. The model generalizes spin-1/2 singlet state probabilities discussed in Czachor (Acta Physica Polonica:139 70–83, 2021) to arbitrary spins _s_. For \(s\rightarrow \infty\) the formalism reduces to ordinary arithmetic and calculus. Accordingly, the limit “non-Newtonian to Newtonian” becomes analogous to the classical limit of a quantum theory.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  14. Unification in a A-Calculus with Intersection Types.Michael Kohlhase & Frank Pfenning - unknown
    We propose related algorithms for unification and constraint simplification in }F’&, a refinement of the simply-typed A-calculus with subtypes and bounded intersection types. }F""’ is intended as the basis of a logical framework in order to achieve more succinct and declarative axiomatiza-.
     
    Export citation  
     
    Bookmark  
  15.  35
    A Type-Driven Vector Semantics for Ellipsis with Anaphora Using Lambek Calculus with Limited Contraction.Gijs Wijnholds & Mehrnoosh Sadrzadeh - 2019 - Journal of Logic, Language and Information 28 (2):331-358.
    We develop a vector space semantics for verb phrase ellipsis with anaphora using type-driven compositional distributional semantics based on the Lambek calculus with limited contraction of Jäger. Distributional semantics has a lot to say about the statistical collocation based meanings of content words, but provides little guidance on how to treat function words. Formal semantics on the other hand, has powerful mechanisms for dealing with relative pronouns, coordinators, and the like. Type-driven compositional distributional semantics brings these two models together. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  16.  44
    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 (4 more)  
     
    Export citation  
     
    Bookmark  
  17.  25
    Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
    Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  18. Strong normalization of a typed lambda calculus for intuitionistic bounded linear-time temporal logic.Norihiro Kamide - 2012 - Reports on Mathematical Logic:29-61.
     
    Export citation  
     
    Bookmark  
  19. Typed lambda calculus.Henk P. Barendregt, Wil Dekkers & Richard Statman - 1977 - In Jon Barwise, Handbook of mathematical logic. New York: North-Holland. pp. 1091--1132.
     
    Export citation  
     
    Bookmark   5 citations  
  20.  24
    Non-idempotent intersection types for the Lambda-Calculus.Antonio Bucciarelli, Delia Kesner & Daniel Ventura - 2017 - Logic Journal of the IGPL 25 (4):431-464.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  21.  33
    On a modal-type language for the predicate calculus.Dimiter Skordev - 1984 - Bulletin of the Section of Logic 13 (3):111-116.
    In order to avoid the use of individual variables in predicate calculus, several authors proposed language whose expressions can be interpreted, in general, as denotations of predicates . The present author also proposed a language of this kind [5]. The absence of individual variables makes all these languages rather different from the traditional language of predicate calculus and from the usual language of mathematics. The translation procedures from the ordinary predicate languages into the predicate languages without individual variables (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  22.  36
    1 The type free λρ-calculus.Yuichi Komori & Arato Cho - 2002 - Bulletin of the Section of Logic 31 (2):65-70.
    Direct download  
     
    Export citation  
     
    Bookmark  
  23.  42
    Three Types and Traditions of Logic: Syllogistic, Calculus and Predicate Logic.Wolfgang Kienzler - 2018 - In Gabriele Mras, Paul Weingartner & Bernhard Ritter, Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin, Boston: De Gruyter. pp. 133-152.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  24.  75
    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 familiar (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  25.  64
    A sequent calculus for type assignment.Jonathan P. Seldin - 1977 - Journal of Symbolic Logic 42 (1):11-28.
  26.  42
    Extracting BB′IW Inhabitants of Simple Types From Proofs in the Sequent Calculus $${LT_\to^{t}}$$ L T → t for Implicational Ticket Entailment.Katalin Bimbó & J. Michael Dunn - 2014 - Logica Universalis 8 (2):141-164.
    The decidability of the logic of pure ticket entailment means that the problem of inhabitation of simple types by combinators over the base { B, B′, I, W } is decidable too. Type-assignment systems are often formulated as natural deduction systems. However, our decision procedure for this logic, which we presented in earlier papers, relies on two sequent calculi and it does not yield directly a combinator for a theorem of ${T_\to}$. Here we describe an algorithm to extract an inhabitant (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  40
    Sequent calculus for 3-valued paraconsistent logic QMPT0.Naoyuki Nide, Yuki Goto & Megumi Fujita - 2019 - Logic Journal of the IGPL 27 (4):507-521.
    We present a sequent calculus of a paraconsistent logic QMPT0, which has the paraconsistent-type excluded middle law (PEML) as an initial sequent. Our system shows that the presence of PEML is essentially important for QMPT0. It also has special rules when the set of constant symbols is finite. We also discuss the cut-elimination property of our system.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  28.  53
    Types in logic and mathematics before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
    In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  29. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - forthcoming - Journal of Logic and Computation.
    In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  30.  24
    (1 other version)Calculuses and formal systems.Haskell B. Curry - 1958 - Dialectica 12 (3‐4):249-273.
    Lorenzen, in his book Einführung in die operative Logik und Mathematik has given a relatively precise form of syntactical system which he calls a calculus. The present paper deals with the relationship of Lorenzen's notion of calculus with the notion of formal system . It is shown that the obs of a formal system can be represented as the theses of a calculus of a certain type just when the calculus has a property called the tectonic (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  64
    Modal pure type systems.Tijn Borghuis - 1998 - Journal of Logic, Language and Information 7 (3):265-296.
    We present a framework for intensional reasoning in typed -calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a propositions-as-types-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  32.  25
    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 (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  46
    A sequent calculus formulation of type assignment with equality rules for the \ambdaβ-calculus.Jonathan P. Seldin - 1978 - Journal of Symbolic Logic 43 (4):643-649.
  34.  25
    On the λY calculus.Rick Statman - 2004 - Annals of Pure and Applied Logic 130 (1-3):325-337.
    The λY calculus is the simply typed λ calculus augmented with the fixed point operators. We show three results about λY: the word problem is undecidable, weak normalisability is decidable, and higher type fixed point operators are not definable from fixed point operators at smaller types.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  35.  40
    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 (4 more)  
     
    Export citation  
     
    Bookmark  
  36.  25
    A General Type for Storage Operators.Karim Nour - 1995 - Mathematical Logic Quarterly 41 (4):505-514.
    In 1990, J.L. Krivine introduced the notion of storage operator to simulate, in $lambda$-calculus, the 'call by value' in a context of a 'call by name'. J.L. Krivine has shown that, using Gödel translation from classical into intuitionistic logic, we can find a simple type for storage operators in AF2 type system. In this present paper, we give a general type for storage operators in a slight extension of AF2. We give at the end (without proof) a generalization of (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  37.  13
    On Involutive Nonassociative Lambek Calculus.Wojciech Buszkowski - 2019 - Journal of Logic, Language and Information 28 (2):157-181.
    Involutive Nonassociative Lambek Calculus is a nonassociative version of Noncommutative Multiplicative Linear Logic, but the multiplicative constants are not admitted. InNL adds two linear negations to Nonassociative Lambek Calculus ; it is a strongly conservative extension of NL Logical aspects of computational linguistics. LNCS, vol 10054. Springer, Berlin, pp 68–84, 2016). Here we also add unary modalities satisfying the residuation law and De Morgan laws. For the resulting logic InNLm, we define and study phase spaces. We use them (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  38.  37
    Calculus CL as Ontology Editor and Inference Engine.Jens Lemanski - 2018 - In Peter Chapman, Gem Stapleton, Amirouche Moktefi, Sarah Perez-Kriz & Francesco Bellucci, Diagrammatic Representation and Inference10th International Conference, Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings. Cham, Switzerland: Springer-Verlag. pp. 752-756.
    The paper outlines the advantages and limits of the so-called ‘Calculus CL’ in the field of ontology engineering and automated theorem proving. CL is a diagram type that combines features of tree, Euler-type, Venn-type diagrams and squares of opposition. Due to the simple taxonomical structures and intuitive rules of CL, it is easy to edit ontologies and to prove inferences.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  39.  60
    The Displacement Calculus.Glyn Morrill, Oriol Valentín & Mario Fadda - 2011 - Journal of Logic, Language and Information 20 (1):1-48.
    If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  40.  46
    Types and Functions since Principia.Fairouz Kamareddine - unknown
    Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell ’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus. Currently, types and functions are the heart of logic and computation and not only are they so closely intertwined, but their evolution (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  41.  44
    Lambek calculus with restricted contraction and expansion.Andreja Prijatelj - 1992 - Studia Logica 51 (1):125 - 143.
    This paper deals with some strengthenings of the non-directional product-free Lambek calculus by means of additional structural rules. In fact, the rules contraction and expansion are restricted to basic types. For each of the presented systems the usual proof-theoretic notions are discussed, some new concepts especially designed for these calculi are introduced reflecting their intermediate position between the weaker and the stronger sequent-systems.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  42.  27
    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.
  43.  30
    Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework.Norihiro Kamide - 2019 - Logica Universalis 13 (1):37-63.
    Gentzen-type sequent calculi GBD+, GBDe, GBD1, and GBD2 are respectively introduced for De and Omori’s axiomatic extensions BD+, BDe, BD1, and BD2 of Belnap–Dunn logic by adding classical negation. These calculi are constructed based on a small modification of the original characteristic axiom scheme for negated implication. Theorems for syntactically and semantically embedding these calculi into a Gentzen-type sequent calculus LK for classical logic are proved. The cut-elimination, decidability, and completeness theorems for these calculi are obtained using these embedding (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  44.  43
    A Bitstring Semantics for Calculus CL.Fabien Schang & Jens Lemanski - 2022 - In Jean-Yves Beziau & Ioannis Vandoulakis, The Exoteric Square of Opposition. Birkhauser. pp. 171–193.
    The aim of this chapter is to develop a semantics for Calculus CL. CL is a diagrammatic calculus based on a logic machine presented by Johann Christian Lange in 1714, which combines features of Euler-, Venn-type, tree diagrams, squares of oppositions etc. In this chapter, it is argued that a Boolean account of formal ontology in CL helps to deal with logical oppositions and inferences of extended syllogistics. The result is a combination of Lange’s diagrams with an algebraic (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  45.  86
    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  
     
    Bookmark  
  46.  19
    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. The Region Connection Calculus, Euler Diagrams and Aristotelian Diagrams (14th edition).Claudia Anger & Lorenz Demey - 2024 - In Jens Lemanski, Mikkel Willum Johansen, Emmanuel Manalo, Petrucio Viana, Reetu Bhattacharjee & Richard Burns, Diagrammatic Representation and Inference 14th International Conference, Diagrams 2024, Münster, Germany, September 27 – October 1, 2024, Proceedings. Cham: Springer. pp. 476-479.
    The Region Connection Calculus (RCC) is a qualitative spatial reasoning formalism, developed in knowledge representation and geographical information systems. We argue that RCC can be viewed as a more fine-grained approach to the use of Euler diagrams to visualize categorical statements like ‘all A are B’. We present RCC using the syntax of first-order modal logic and a topological semantics. We compare the Gergonne relations (a well-known set of 5 jointly exhaustive and pairwise disjoint relations between two non-empty sets, (...)
    No categories
     
    Export citation  
     
    Bookmark  
  48.  56
    Resolution calculus for the first order linear logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
    This paper presents a formulation and completeness proof of the resolution-type calculi for the first order fragment of Girard's linear logic by a general method which provides the general scheme of transforming a cutfree Gentzen-type system into a resolution type system, preserving the structure of derivations. This is a direct extension of the method introduced by Maslov for classical predicate logic. Ideas of the author and Zamov are used to avoid skolomization. Completeness of strategies is first established for the Gentzen-type (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  49.  42
    Strong normalization in type systems: A model theoretical approach.Jan Terlouw - 1995 - Annals of Pure and Applied Logic 73 (1):53-78.
    Tait's proof of strong normalization for the simply typed λ-calculus is interpreted in a general model theoretical framework by means of the specification of a certain theory T and a certain model /oU of T. The argumentation is partly reduced to formal predicate logic by the application of certain derivability properties of T. The resulting version of Tait's proof is, within the same framework, systematically generalized to the Calculus of Constructions and other advanced type systems. The generalization (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  50.  41
    Prototype Proofs in Type Theory.Giuseppe Longo - 2000 - Mathematical Logic Quarterly 46 (2):257-266.
    The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ-calculus and act as “proof-schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type Theory, i. e. (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
1 — 50 / 927