Search results for 'Type theory' (try it on Scholar)

1000+ found
Sort by:
  1. P. B. Andrews (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Kluwer Academic Publishers.score: 240.0
    This introduction to mathematical logic starts with propositional calculus and first-order logic. Topics covered include syntax, semantics, soundness, completeness, independence, normal forms, vertical paths through negation normal formulas, compactness, Smullyan's Unifying Principle, natural deduction, cut-elimination, semantic tableaux, Skolemization, Herbrand's Theorem, unification, duality, interpolation, and definability. The last three chapters of the book provide an introduction to type theory (higher-order logic). It is shown how various mathematical concepts can be formalized in this very expressive formal language. This expressive notation (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  2. Maria van der Schaar (2011). The Cognitive Act and the First-Person Perspective: An Epistemology for Constructive Type Theory. [REVIEW] Synthese 180 (3):391-417.score: 240.0
    The notion of cognitive act is of importance for an epistemology that is apt for constructive type theory, and for epistemology in general. Instead of taking knowledge attributions as the primary use of the verb ‘to know’ that needs to be given an account of, and understanding a first-person knowledge claim as a special case of knowledge attribution, the account of knowledge that is given here understands first-person knowledge claims as the primary use of the verb ‘to know’. (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Salvatore Florio & Stewart Shapiro (2014). Set Theory, Type Theory, and Absolute Generality. Mind 123 (489):157-174.score: 240.0
    In light of the close connection between the ontological hierarchy of set theory and the ideological hierarchy of type theory, Øystein Linnebo and Agustín Rayo have recently offered an argument in favour of the view that the set-theoretic universe is open-ended. In this paper, we argue that, since the connection between the two hierarchies is indeed tight, any philosophical conclusions cut both ways. One should either hold that both the ontological hierarchy and the ideological hierarchy are open-ended, (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Maria Schaar (2011). Assertion and Grounding: A Theory of Assertion for Constructive Type Theory. Synthese 183 (2):187-210.score: 240.0
    Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of demonstration. (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  5. Johan Georg Granström (2011). Treatise on Intuitionistic Type Theory. Springer.score: 240.0
    Prolegomena It is fitting to begin this book on intuitionistic type theory by putting the subject matter into perspective. The purpose of this chapter is to ...
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Giuseppe Primiero & Mariarosiaria Taddeo (2012). A Modal Type Theory for Formalizing Trusted Communications. Journal of Applied Logic 10 (1):92-114.score: 240.0
    This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  7. André Fuhrmann (2010). Russell´s Early Type Theory and the Paradox of Propositions. Principia 5 (1-2):19-42.score: 240.0
    The paradox of propositiOns, presented in Appenclix B of Russell's The Principies of Mathernatics (1903), is usually taken as Russell's principal motive, at the time, for moving from a simple to a ramified theory of types. I argue that this view is mistaken. A closer study of Russell's correspondence with Frege reveals that Russell carne to adopt a very different resolution of the paradox, calling into question not the simplicity of his early type theory but the simplicity (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  8. Iris Loeb (2014). Towards Transfinite Type Theory: Rereading Tarski's Wahrheitsbegriff. Synthese 191 (10):2281-2299.score: 240.0
    In his famous paper Der Wahrheitsbegriff in den formalisierten Sprachen (Polish edition: Nakładem/Prace Towarzystwa Naukowego Warszawskiego, wydzial, III, 1933), Alfred Tarski constructs a materially adequate and formally correct definition of the term “true sentence” for certain kinds of formalised languages. In the case of other formalised languages, he shows that such a construction is impossible but that the term “true sentence” can nevertheless be consistently postulated. In the Postscript that Tarski added to a later version of this paper (Studia Philosophica, (...)
    No categories
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  9. Christoph Benzmüller & Lawrence C. Paulson (2013). Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7 (1):7-20.score: 240.0
    We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  10. Erik Palmgren (2012). Proof-Relevance of Families of Setoids and Identity in Type Theory. Archive for Mathematical Logic 51 (1-2):35-47.score: 240.0
    Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  11. Maria van der Schaar (2011). Assertion and Grounding: A Theory of Assertion for Constructive Type Theory. Synthese 183 (2):187-210.score: 240.0
    Taking Per Martin-Löf’s constructive type theory as a starting-point a theory of assertion is developed, which is able to account for the epistemic aspects of the speech act of assertion, and in which it is shown that assertion is not a wide genus. From a constructivist point of view, one is entitled to assert, for example, that a proposition A is true, only if one has constructed a proof object a for A in an act of demonstration. (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  12. Giuseppe Primiero (2012). A Contextual Type Theory with Judgemental Modalities for Reasoning From Open Assumptions. Logique and Analyse 220:579-600.score: 224.0
    Contextual type theories are largely explored in their applications to programming languages, but less investigated for knowledge representation purposes. The combination of a constructive language with a modal extension of contexts appears crucial to explore the attractive idea of a type-theoretical calculus of provability from refutable assumptions for non-monotonic reasoning. This paper introduces such a language: the modal operators are meant to internalize two different modes of correctness, respectively with necessity as the standard notion of constructive verification and (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  13. Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano (2013). Completeness in Hybrid Type Theory. Journal of Philosophical Logic (2-3):1-30.score: 216.0
    We show that basic hybridization (adding nominals and @ operators) makes it possible to give straightforward Henkin-style completeness proofs even when the modal logic being hybridized is higher-order. The key ideas are to add nominals as expressions of type t, and to extend to arbitrary types the way we interpret $@_i$ in propositional and first-order hybrid logic. This means: interpret $@_i\alpha _a$ , where $\alpha _a$ is an expression of any type $a$ , as an expression of (...) $a$ that rigidly returns the value that $\alpha_a$ receives at the i-world. The axiomatization and completeness proofs are generalizations of those found in propositional and first-order hybrid logic, and (as is usual inhybrid logic) we automatically obtain a wide range of completeness results for stronger logics and languages. Our approach is deliberately low-tech. We don’t, for example, make use of Montague’s intensional type s, or Fitting-style intensional models; we build, as simply as we can, hybrid logicover Henkin’s logic. (shrink)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  14. Giovanni Sambin & Jan M. Smith (eds.) (1998). Twenty-Five Years of Constructive Type Theory: Proceedings of a Congress Held in Venice, October 1995. Oxford University Press.score: 216.0
    This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Lof over the last twenty-five years.
    Direct download  
     
    My bibliography  
     
    Export citation  
  15. Carlos Areces, Patrick Blackburn, Antonia Huertas & María Manzano (2012). Hybrid Type Theory: A Quartet in Four Movements. Principia 15 (2):225.score: 210.0
    Este artigo canta uma canção — uma canção criada ao unir o trabalho de quatro grandes nomes na história da lógica: Hans Reichenbach, Arthur Prior, Richard Montague, e Leon Henkin. Embora a obra dos primeiros três desses autores tenha sido previamente combinada, acrescentar as ideias de Leon Henkin é o acréscimo requerido para fazer com que essa combinação funcione no nível lógico. Mas o presente trabalho não se concentra nas tecnicalidades subjacentes (que podem ser encontradas em Areces, Blackburn, Huertas, e (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  16. Erik Palmgren (1995). The Friedman‐Translation for Martin‐Löf's Type Theory. Mathematical Logic Quarterly 41 (3):314-326.score: 210.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  17. Silvio Valentini (1996). Decidability in Intuitionistic Type Theory is Functionally Decidable. Mathematical Logic Quarterly 42 (1):300-304.score: 210.0
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  18. Andrey A. Kuzichev (1992). The Ambiguous Type Theory is Hereditarily Undecidable. Mathematical Logic Quarterly 38 (1):299-300.score: 210.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  19. G. Longo (2000). Prototype Proofs in Type Theory. Mathematical Logic Quarterly 46 (2):257-266.score: 210.0
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  20. P. B. Andrews (1965). A Transfinite Type Theory with Type Variables. Amsterdam, North-Holland Pub. Co..score: 210.0
    No categories
     
    My bibliography  
     
    Export citation  
  21. Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.score: 192.0
    In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  22. Fairouz Kamareddine (1995). A Type Free Theory and Collective/Distributive Predication. Journal of Logic, Language and Information 4 (2):85-109.score: 192.0
    The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  23. J. Lambek & P. J. Scott (1981). Intuitionist Type Theory and Foundations. Journal of Philosophical Logic 10 (1):101 - 115.score: 180.0
    A version of intuitionistic type theory is presented here in which all logical symbols are defined in terms of equality. This language is used to construct the so-called free topos with natural number object. It is argued that the free topos may be regarded as the universe of mathematics from an intuitionist's point of view.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  24. Steve Awodey, Type Theory and Homotopy.score: 180.0
    of type theory has been used successfully to formalize large parts of constructive mathematics, such as the theory of generalized recursive definitions [NPS90, ML79]. Moreover, it is also employed extensively as a framework for the development of high-level programming languages, in virtue of its combination of expressive strength and desirable proof-theoretic properties [NPS90, Str91]. In addition to simple types A, B, . . . and their terms x : A b(x) : B, the theory also has (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  25. J. Michael Dunn (1979). A Theorem in 3-Valued Model Theory with Connections to Number Theory, Type Theory, and Relevant Logic. Studia Logica 38 (2):149 - 169.score: 180.0
    Given classical (2 valued) structures and and a homomorphism h of onto , it is shown how to construct a (non-degenerate) 3-valued counterpart of . Classical sentences that are true in are non-false in . Applications to number theory and type theory (with axiom of infinity) produce finite 3-valued models in which all classically true sentences of these theories are non-false. Connections to relevant logic give absolute consistency proofs for versions of these theories formulated in relevant logic (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  26. Edward N. Zalta (1982). Meinongian Type Theory and its Applications. Studia Logica 41 (2-3):297-307.score: 180.0
    <span class='Hi'></span> In this paper I propose a fundamental modification of standard type theory,<span class='Hi'></span> produce a new kind of type theoretic language,<span class='Hi'></span> and couch in this language a comprehensive theory of abstract individuals and abstract properties and relations of every type.<span class='Hi'></span> I then suggest how to employ the theory to solve the four following philosophical problems:<span class='Hi'></span> (A)<span class='Hi'></span> the identification and ontological status of Frege's Senses;<span class='Hi'></span> (B)<span class='Hi'></span> the deviant (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  27. G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.score: 180.0
    We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  28. Robin Cooper, Austinian Truth, Attitudes and Type Theory ∗.score: 180.0
    This paper is part of a broader project whose aim is to present a coherent unified approach to natural language dialogue semantics using tools from type theory. Here we explore aspects of our approach which relate to situation theory and situation semantics. We first point out a relationship between type theory and the Austinian notion of truth. We then consider how records in type theory might be used to represent situations and how dependent (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  29. Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.score: 180.0
    Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  30. Adam Obtułowicz (1989). Categorical and Algebraic Aspects of Martin-Löf Type Theory. Studia Logica 48 (3):299 - 317.score: 180.0
    In the paper there are introduced and discussed the concepts of an indexed category with quantifications and a higher level indexed category to present an algebraic characterization of some version of Martin-Löf Type Theory. This characterization is given by specifying an additional equational structure of those indexed categories which are models of Martin-Löf Type Theory. One can consider the presented characterization as an essentially algebraic theory of categorical models of Martin-Löf Type Theory. The (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  31. Georg Schiemer & Erich H. Reck (2013). Logic in the 1930s: Type Theory and Model Theory. Bulletin of Symbolic Logic 19 (4):433-472.score: 180.0
    In historical discussions of twentieth-century logic, it is typically assumed that model theory emerged within the tradition that adopted first-order logic as the standard framework. Work within the type-theoretic tradition, in the style of Principia Mathematica, tends to be downplayed or ignored in this connection. Indeed, the shift from type theory to first-order logic is sometimes seen as involving a radical break that first made possible the rise of modern model theory. While comparing several early (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  32. Jesper Carlström (2005). Interpreting Descriptions in Intensional Type Theory. Journal of Symbolic Logic 70 (2):488 - 514.score: 180.0
    Natural deduction systems with indefinite and definite descriptions (ε-terms and ι-terms) are presented, and interpreted in Martin-Löf's intensional type theory. The interpretations are formalizations of ideas which are implicit in the literature of constructive mathematics: if we have proved that an element with a certain property exists, we speak of 'the element such that the property holds' and refer by that phrase to the element constructed in the existence proof. In particular, we deviate from the practice of interpreting (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Zofia Kostrzycka & Marek Zaionc (2008). Asymptotic Densities in Logic and Type Theory. Studia Logica 88 (3):385 - 403.score: 180.0
    This paper presents a systematic approach for obtaining results from the area of quantitative investigations in logic and type theory. We investigate the proportion between tautologies (inhabited types) of a given length n against the number of all formulas (types) of length n. We investigate an asymptotic behavior of this fraction. Furthermore, we characterize the relation between number of premises of implicational formula (type) and the asymptotic probability of finding such formula among the all ones. We also (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  34. Robin Cooper, Type Theory with Records and Unification-Based Grammar.score: 180.0
    We suggest a way of bringing together type theory and unification-based grammar formalisms by using records in type theory. The work is part of a broader project whose aim is to present a coherent unified approach to natural language dialogue semantics using tools from type theory.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  35. M. D. G. Swaen (1991). The Logic of First Order Intuitionistic Type Theory with Weak Sigma- Elimination. Journal of Symbolic Logic 56 (2):467-483.score: 180.0
    Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HA ω into a type theory WL, that can be described as Troelstra's system ML 1 0 with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HA ω if and only if its corresponding type in WL is inhabited. Analogous results are (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  36. Steve Awodey, Natural Models of Homotopy Type Theory.score: 180.0
    The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π, and intensional identity types (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  37. Edwin D. Mares (2007). The Fact Semantics for Ramified Type Theory and the Axiom of Reducibility. Notre Dame Journal of Formal Logic 48 (2):237-251.score: 180.0
    This paper uses an atomistic ontology of universals, individuals, and facts to provide a semantics for ramified type theory. It is shown that with some natural constraints on the sort of universals and facts admitted into a model, the axiom of reducibility is made valid.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  38. M. Randall Holmes, Polymorphic Type Checking for the Type Theory of the Principia Mathematica of Russell and Whitehead.score: 180.0
    This is a brief report on results reported at length in our paper [2], made for the purpose of a presentation at the workshop to be held in November 2011 in Cambridge on the Principia Mathematica of Russell and Whitehead ([?], hereinafter referred to briefly as PM ). That paper grew out of a reading of the paper [3] of Kamareddine, Nederpelt, and Laan. We refereed this paper and found it useful for checking their examples to write our own independent (...)
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  39. Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. Journal of Symbolic Logic 49 (3):730-753.score: 180.0
    We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  40. Maria van der Schaar (2011). The Cognitive Act and the First-Person Perspective: An Epistemology for Constructive Type Theory. Synthese 180 (3):391 - 417.score: 180.0
    The notion of cognitive act is of importance for an epistemology that is apt for constructive type theory, and for epistemology in general. Instead of taking knowledge attributions as the primary use of the verb 'to know' that needs to be given an account of, and understanding a first-person knowledge claim as a special case of knowledge attribution, the account of knowledge that is given here understands first-person knowledge claims as the primary use of the verb 'to know'. (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  41. Anton Setzer (2000). Extending Martin-Löf Type Theory by One Mahlo-Universe. Archive for Mathematical Logic 39 (3):155-181.score: 180.0
    We define a type theory MLM, which has proof theoretical strength slightly greater then Rathjen's theory KPM. This is achieved by replacing the universe in Martin-Löf's Type Theory by a new universe V having the property that for every function f, mapping families of sets in V to families of sets in V, there exists a universe inside V closed under f. We show that the proof theoretical strength of MLM is $\geq \psi_{\Omega_1}\Omega_{{\rm M}+\omega}$ . (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  42. Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65 (2):525-549.score: 180.0
    The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe á la Tarski. A set U 0 of codes for small sets is generated inductively at the same time as a function T 0 , which maps a code to the corresponding small set, is defined by recursion on the way the elements of U 0 are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  43. Michael Rathjen (2000). The Strength of Martin-Löf Type Theory with a Superuniverse. Part I. Archive for Mathematical Logic 39 (1):1-39.score: 180.0
    Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  44. Michael Rathjen (2001). The Strength of Martin-Löf Type Theory with a Superuniverse. Part II. Archive for Mathematical Logic 40 (3):207-233.score: 180.0
    Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  45. Joseph L. Pe (1992). Polynomial-Time Martin-Löf Type Theory. Archive for Mathematical Logic 32 (2):137-150.score: 180.0
    Fragments of extensional Martin-Löf type theory without universes,ML 0, are introduced that conservatively extend S.A. Cook and A. Urquhart'sIPV ω. A model for these restricted theories is obtained by interpretation in Feferman's theory APP of operators, a natural model of which is the class of partial recursive functions. In conclusion, some examples in group theory are considered.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  46. Michael Rathjen (2003). Realizing Mahlo Set Theory in Type Theory. Archive for Mathematical Logic 42 (1):89-101.score: 180.0
    After introducing the large set notion of Mahloness, this paper shows that constructive set theory with an axiom asserting the existence of a Mahlo set has a realizability interpretation in an extension of Martin-Löf type theory developed by A. Setzer.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  47. Geir Waagbø (1999). Denotational Semantics for Intuitionistic Type Theory Using a Hierarchy of Domains with Totality. Archive for Mathematical Logic 38 (1):19-60.score: 180.0
    A modified version of Normann's hierarchy of domains with totality [9] is presented and is shown to be suitable for interpretation of Martin-Löf's intuitionistic type theory. This gives an interpretation within classical set theory, which is natural in the sense that $\Sigma$ -types are interpreted as sets of pairs and $\Pi$ -types as sets of choice functions. The hierarchy admits a natural definition of the total objects in the domains, and following an idea of Berger [3] this (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  48. Stephen H. Voss & Charles Sayward (1980). The Structure of Type Theory. Journal of Philosophy 77 (5):241-259.score: 174.0
    Formal principals are isolated to reveal a structure embedded in a wide range of studies, each of which partitions a domain of individuals into types and categories. It is thought that any reasonable theory of types should include these principles.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  49. Ingrid Lindström (1989). A Construction of Non-Well-Founded Sets Within Martin-Löf's Type Theory. Journal of Symbolic Logic 54 (1):57-64.score: 174.0
    In this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löf's theory of types. A system is a type W together with an assignment of ᾱ ∈ U and α̃ ∈ ᾱ → W to each α ∈ W. We show that for any system W we can define an equivalence relation = w such that α = w β ∈ U and = w is the maximal bisimulation. (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  50. Paul C. Gilmore (2001). An Intensional Type Theory: Motivation and Cut-Elimination. Journal of Symbolic Logic 66 (1):383-400.score: 174.0
    By the theory TT is meant the higher order predicate logic with the following recursively defined types: (1) 1 is the type of individuals and [] is the type of the truth values: (2) [τ l ,..., τ n ] is the type of the predicates with arguments of the types τ l ,..., τ n . The theory ITT described in this paper is an intensional version of TT. The types of ITT are the (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000