Bibliographies thématiques / Martin-Löf Type Theory / Articles de revues

Articles de revues sur le sujet « Martin-Löf Type Theory »

Pour voir les autres types de publications sur ce sujet consultez le lien suivant : Martin-Löf Type Theory.
Auteur : Grafiati
Publié le 11 mars 2023

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les 44 meilleurs articles de revues pour votre recherche sur le sujet « Martin-Löf Type Theory ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Parcourez les articles de revues sur diverses disciplines et organisez correctement votre bibliographie.

1

Gambino, Nicola, et Peter Aczel. « The generalised type-theoretic interpretation of constructive set theory ». Journal of Symbolic Logic 71, no 1 (juin 2006) : 67–103. http://dx.doi.org/10.2178/jsl/1140641163.

Texte intégral
Résumé :
AbstractWe present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
Styles APA, Harvard, Vancouver, ISO, etc.
2

KLEV, ANSTEN. « ETA-RULES IN MARTIN-LÖF TYPE THEORY ». Bulletin of Symbolic Logic 25, no 03 (22 juillet 2019) : 333–59. http://dx.doi.org/10.1017/bsl.2019.21.

Texte intégral
Résumé :
AbstractThe eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher order eta rule is part of that type theory. The main aim of this article is to clarify this somewhat puzzling situation. It will be argued that lower order eta rules do not, whereas the higher order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.
Styles APA, Harvard, Vancouver, ISO, etc.
3

Lamarche, François. « Modeling Martin-Löf type theory in categories ». Journal of Applied Logic 12, no 1 (mars 2014) : 28–44. http://dx.doi.org/10.1016/j.jal.2013.08.003.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
4

AWODEY, STEVE, et MICHAEL A. WARREN. « Homotopy theoretic models of identity types ». Mathematical Proceedings of the Cambridge Philosophical Society 146, no 1 (janvier 2009) : 45–55. http://dx.doi.org/10.1017/s0305004108001783.

Texte intégral
Résumé :
Quillen [17] introduced model categories as an abstract framework for homotopy theory which would apply to a wide range of mathematical settings. By all accounts this program has been a success and—as, e.g., the work of Voevodsky on the homotopy theory of schemes [15] or the work of Joyal [11,12] and Lurie [13] on quasicategories seem to indicate—it will likely continue to facilitate mathematical advances. In this paper we present a novel connection between model categories and mathematical logic, inspired by the groupoid model of (intensional) Martin–Löf type theory [14] due to Hofmann and Streicher [9]. In particular, we show that a form of Martin–Löf type theory can be soundly modelled in any model category. This result indicates moreover that any model category has an associated “internal language” which is itself a form of Martin-Löf type theory. This suggests applications both to type theory and to homotopy theory. Because Martin–Löf type theory is, in one form or another, the theoretical basis for many of the computer proof assistants currently in use, such asCoqandAgda(cf. [3] and [5]), this promise of applications is of a practical, as well as theoretical, nature.
Styles APA, Harvard, Vancouver, ISO, etc.
5

GARNER, RICHARD. « Two-dimensional models of type theory ». Mathematical Structures in Computer Science 19, no 4 (août 2009) : 687–736. http://dx.doi.org/10.1017/s0960129509007646.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
6

Obtułowicz, Adam. « Algebra of constructions II : an algebraic approach to Martin-Löf type theory and the calculus of constructions ». Mathematical Structures in Computer Science 3, no 1 (mars 1993) : 63–92. http://dx.doi.org/10.1017/s0960129500000128.

Texte intégral
Résumé :
We present an algebraic approach to the syntax and semantics of Martin-Löf type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are treated as three-sorted partial algebras, called ITSΠ-structures, described by essentially algebraic theories. We give a proof that derived statements of Martin-Löf type theory hold in appropriate ITSΠ-structures. In this proof, a formal translation from the language of terms and types into the language of terms of an appropriate essentially algebraic theory of ITSΠ-structures is used. A straightforward set-theoretic construction of ITSΠ-structures that are models of Martin-Löf type theory is demonstrated. We present a construction of a recursive ITSΠ-structure(i.e. its partial and total operations are recursive functions over some alphabet) that is a model of the calculus of constructions and demonstrates the decidability of this calculus.
Styles APA, Harvard, Vancouver, ISO, etc.
7

Palmgren, Erik. « A construction of type : type in Martin-Löf's partial type theory with one universe ». Journal of Symbolic Logic 56, no 3 (septembre 1991) : 1012–15. http://dx.doi.org/10.2307/2275068.

Texte intégral
Résumé :
In this note we construct Martin-Löf's inconsistent type theory, Type: Type (Martin-Löf [1971]), inside partial type theory with one universe. Thus adding a fixed point operator to type theory with one predicative universe gives impredicativity.We may describe the theory Type:Type as follows. It contains the rules for the product construction (II) of Martin-Löf [1984] except the η-rule and it contains the usual rules for definitional equality (=). Moreover it contains the following strongly impredicative universeThis theory is inconsistent (i.e. every set is inhabited), and this is seen by proving a variant of the Burali—Forti paradox—Girard's paradox—cf. Troelstra and van Dalen [1988]. Coquand [199?] has shown that by adding the well-order type and the strong dependent sum to the universe, the fixed point operator becomes definable. It is an open problem whether it is definable without the well-order type. The present result could be seen as a converse, namely by adding the fixed point operator to type theory with one universe, Type:Type becomes definable and, as is already known, so does the well-order type.
Styles APA, Harvard, Vancouver, ISO, etc.
8

Setzer, Anton. « Well-ordering proofs for Martin-Löf type theory ». Annals of Pure and Applied Logic 92, no 2 (mai 1998) : 113–59. http://dx.doi.org/10.1016/s0168-0072(97)00078-x.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
9

Setzer, Anton. « Extending Martin-Löf Type Theory by one Mahlo-universe ». Archive for Mathematical Logic 39, no 3 (1 avril 2000) : 155–81. http://dx.doi.org/10.1007/s001530050140.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
10

Obtułowicz, Adam. « Categorical and algebraic aspects of Martin-Löf Type Theory ». Studia Logica 48, no 3 (septembre 1989) : 299–317. http://dx.doi.org/10.1007/bf00370827.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
11

Rathjen, Michael, et Sergei Tupailo. « Characterizing the interpretation of set theory in Martin-Löf type theory ». Annals of Pure and Applied Logic 141, no 3 (septembre 2006) : 442–71. http://dx.doi.org/10.1016/j.apal.2005.12.008.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
12

Domanov, Oleg. « FUZZY TYPE THEORY IN THE ANALYSIS OF ARGUMENTATION ». Respublica literaria, RL. 2021. vol.2. no. 1 (29 mars 2021) : 37–47. http://dx.doi.org/10.47850/rl.2021.2.1.37-47.

Texte intégral
Résumé :
The article deals with a fazzy variant of P. Martin-Löf ’s intuitionistic type theory. It presents the overview of fuzzy type theory rules and an example of its application to the analysis of the persuasiveness of argumentation. In the latter, the truth values of fuzzy logic are interpreted as degrees of persuasiveness of statements and arguments. The formalization is implemented in the proof assistant Agda.
Styles APA, Harvard, Vancouver, ISO, etc.
13

Rodin, Andrei V. « Martin-Löf Type Theory as a Multi-Agent Epistemic Formal System ». Epistemology & ; Philosophy of Science 55, no 4 (2018) : 44–47. http://dx.doi.org/10.5840/eps201855464.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
14

Abel, Andreas, Klaus Aehlig et Peter Dybjer. « Normalization by Evaluation for Martin-Löf Type Theory with One Universe ». Electronic Notes in Theoretical Computer Science 173 (avril 2007) : 17–39. http://dx.doi.org/10.1016/j.entcs.2007.02.025.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
15

Bunder, M. W. « Possible forms of evaluation or reduction in Martin-Löf type theory ». Theoretical Computer Science 41 (1985) : 113–20. http://dx.doi.org/10.1016/0304-3975(85)90065-9.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
16

GYLTERUD, HÅKON ROBBESTAD. « FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY ». Journal of Symbolic Logic 83, no 3 (septembre 2018) : 1132–46. http://dx.doi.org/10.1017/jsl.2017.84.

Texte intégral
Résumé :
AbstractWe give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel’s 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of “Homotopy Type Theory” by the Univalent Foundations Program.
Styles APA, Harvard, Vancouver, ISO, etc.
17

BARRAS, BRUNO, THIERRY COQUAND et SIMON HUBER. « A generalization of the Takeuti–Gandy interpretation ». Mathematical Structures in Computer Science 25, no 5 (20 février 2015) : 1071–99. http://dx.doi.org/10.1017/s0960129514000504.

Texte intégral
Résumé :
We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.
Styles APA, Harvard, Vancouver, ISO, etc.
18

Palmgren, Erik. « A note on Mathematics of infinity ». Journal of Symbolic Logic 58, no 4 (décembre 1993) : 1195–200. http://dx.doi.org/10.2307/2275138.

Texte intégral
Résumé :
In the paper Mathematics of infinity, Martin-Löf extends his intuitionistic type theory with fixed “choice sequences”. The simplest, and most important instance, is given by adding the axiomsto the type of natural numbers. Martin-Löf's type theory can be regarded as an extension of Heyting arithmetic (HA). In this note we state and prove Martin-Löf's main result for this choice sequence, in the simpler setting of HA and other arithmetical theories based on intuitionistic logic (Theorem A). We also record some remarkable properties of the resulting systems; in general, these lack the disjunction property and may or may not have the explicit definability property. Moreover, they represent all recursive functions by terms.
Styles APA, Harvard, Vancouver, ISO, etc.
19

Rathjen, Michael. « The strength of Martin-Löf type theory with a superuniverse. Part II ». Archive for Mathematical Logic 40, no 3 (1 avril 2001) : 207–33. http://dx.doi.org/10.1007/s001530000051.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
20

Rathjen, Michael. « The strength of Martin-Löf type theory with a superuniverse. Part I ». Archive for Mathematical Logic 39, no 1 (1 janvier 2000) : 1–39. http://dx.doi.org/10.1007/s001530050001.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
21

Rathjen, Michael. « The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory ». Synthese 147, no 1 (octobre 2005) : 81–120. http://dx.doi.org/10.1007/s11229-004-6208-4.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
22

GYLTERUD, HÅKON ROBBESTAD. « Multisets in type theory ». Mathematical Proceedings of the Cambridge Philosophical Society 169, no 1 (27 mars 2019) : 1–18. http://dx.doi.org/10.1017/s0305004119000045.

Texte intégral
Résumé :
AbstractA multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin–Löf Type Theory, in the presence of Voevodsky’s Univalence Axiom.In his 1978 paper, “the type theoretic interpretation of constructive set theory” Aczel introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the univalence axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.
Styles APA, Harvard, Vancouver, ISO, etc.
23

CARL, MERLIN, et PHILIPP SCHLICHT. « RANDOMNESS VIA INFINITE COMPUTATION AND EFFECTIVE DESCRIPTIVE SET THEORY ». Journal of Symbolic Logic 83, no 2 (juin 2018) : 766–89. http://dx.doi.org/10.1017/jsl.2018.3.

Texte intégral
Résumé :
AbstractWe study randomness beyond${\rm{\Pi }}_1^1$-randomness and its Martin-Löf type variant, which was introduced in [16] and further studied in [3]. Here we focus on a class strictly between${\rm{\Pi }}_1^1$and${\rm{\Sigma }}_2^1$that is given by the infinite time Turing machines (ITTMs) introduced by Hamkins and Kidder. The main results show that the randomness notions associated with this class have several desirable properties, which resemble those of classical random notions such as Martin-Löf randomness and randomness notions defined via effective descriptive set theory such as${\rm{\Pi }}_1^1$-randomness. For instance, mutual randoms do not share information and a version of van Lambalgen’s theorem holds.Towards these results, we prove the following analogue to a theorem of Sacks. If a real is infinite time Turing computable relative to all reals in some given set of reals with positive Lebesgue measure, then it is already infinite time Turing computable. As a technical tool towards this result, we prove facts of independent interest about random forcing over increasing unions of admissible sets, which allow efficient proofs of some classical results about hyperarithmetic sets.
Styles APA, Harvard, Vancouver, ISO, etc.
24

Palmgren, E. « An Information System Interpretation of Martin-Löf′s Partial Type Theory with Universes ». Information and Computation 106, no 1 (septembre 1993) : 26–60. http://dx.doi.org/10.1006/inco.1993.1048.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
25

Garner, Richard. « On the strength of dependent products in the type theory of Martin-Löf ». Annals of Pure and Applied Logic 160, no 1 (juillet 2009) : 1–12. http://dx.doi.org/10.1016/j.apal.2008.12.003.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
26

PALMGREN, ERIK. « A CONSTRUCTIVE EXAMINATION OF A RUSSELL-STYLE RAMIFIED TYPE THEORY ». Bulletin of Symbolic Logic 24, no 1 (mars 2018) : 90–106. http://dx.doi.org/10.1017/bsl.2018.4.

Texte intégral
Résumé :
AbstractIn this article we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell’s reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell’s theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos.
Styles APA, Harvard, Vancouver, ISO, etc.
27

Smith, Jan M. « The independence of Peano's fourth axiom from Martin-Löf's type theory without universes ». Journal of Symbolic Logic 53, no 3 (septembre 1988) : 840–45. http://dx.doi.org/10.2307/2274575.

Texte intégral
Résumé :
In Hilbert and Ackermann [2] there is a simple proof of the consistency of first order predicate logic by reducing it to propositional logic. Intuitively, the proof is based on interpreting predicate logic in a domain with only one element. Tarski [7] and Gentzen [1] have extended this method to simple type theory by starting with an individual domain consisting of a single element and then interpreting a higher type by the set of truth valued functions on the previous type.I will use the method of Hilbert and Ackermann on Martin-Löf's type theory without universes to show that ¬Eq(A, a, b) cannot be derived without universes for any type A and any objects a and b of type A. In particular, this proves the conjecture in Martin-Löf [5] that Peano's fourth axiom (∀x ϵ N)¬ Eq(N, 0, succ(x)) cannot be proved in type theory without universes. If by consistency we mean that there is no closed term of the empty type, then the construction will also give a consistency proof by finitary methods of Martin-Löf's type theory without universes. So, without universes, the logic obtained by interpreting propositions as types is surprisingly weak. This is in sharp contrast with type theory as a computational system, since, for instance, the proof that every object of a type can be computed to normal form cannot be formalized in first order arithmetic.
Styles APA, Harvard, Vancouver, ISO, etc.
28

PISTONE, PAOLO. « POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC : A VICTIMS’ TALE ». Bulletin of Symbolic Logic 24, no 1 (mars 2018) : 1–52. http://dx.doi.org/10.1017/bsl.2017.43.

Texte intégral
Résumé :
AbstractThe investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity (or impredicativity) of second and higher-order logic. However, the epistemological significance of such investigations has not received much attention in the contemporary foundational debate.We discuss Girard’s normalization proof for second order type theory or System F and compare it with two faulty consistency arguments: the one given by Frege for the logical system of the Grundgesetze (shown inconsistent by Russell’s paradox) and the one given by Martin-Löf for the intuitionistic type theory with a type of all types (shown inconsistent by Girard’s paradox).The comparison suggests that the question of the circularity of second order logic cannot be reduced to Russell’s and Poincaré’s 1906 “vicious circle” diagnosis. Rather, it reveals a bunch of mathematical and logical ideas hidden behind the hazardous idea of impredicative quantification, constituting a vast (and largely unexplored) domain for foundational research.
Styles APA, Harvard, Vancouver, ISO, etc.
29

Normann, Dag, Erik Palmgren et Viggo Stoltenberg-Hansen. « Hyperfinite type structures ». Journal of Symbolic Logic 64, no 3 (septembre 1999) : 1216–42. http://dx.doi.org/10.2307/2586626.

Texte intégral
Résumé :
The notion of a hyperfinite set comes from nonstandard analysis. Such a set has the internal cardinality of a nonstandard natural number. By a transfer principle such sets share many properties of finite sets. Here we apply this notion to give a hyperfinite model of the Kleene-Kreisel continuous functionals. We also extend the method to provide a hyperfinite characterisation of certain transfinite type structures, thus, through the work of Waagbø [14], constructing a hyperfinite model for Martin-Löf type theory.This kind of application is not new. Normann [6] gave a characterisation of the Kleene-Kreisel continuous functionals using ‘hyperfinitary’ functionals. The novelty here is that we use a constructive version of hyperfinite functionals and also generalise the method to transfinite types. Many of the results of this paper are constructive, though not the characterisation theorems themselves.Our characterisation of the Kleene-Kreisel continuous functionals is a supplement to a number of previous characterisations of topological and recursion-theoretical nature, see [6] for a brief survey. Altogether these characterisations show that the original concept of Kleene and Kreisel forms the correct mathematical model of the idea of finitely based functions of finite types.There is, however, no a priori reason to believe that there is a canonical way to extend the continuous functionals to cover transfinite objects of transfinite type used in, e.g., type theory. Our characterisation of Waagbø's model indicates that the model is natural, not only seen from domain theory but from a higher perspective. Normann and Waagbø (unpublished) have subsequently obtained a limit-space characterisation that further supports this view.
Styles APA, Harvard, Vancouver, ISO, etc.
30

CHAPMAN, JAMES, TARMO UUSTALU et NICCOLÒ VELTRI. « Quotienting the delay monad by weak bisimilarity ». Mathematical Structures in Computer Science 29, no 1 (17 octobre 2017) : 67–92. http://dx.doi.org/10.1017/s0960129517000184.

Texte intégral
Résumé :
The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.
Styles APA, Harvard, Vancouver, ISO, etc.
31

Buchholz, Wilfried. « Anton Setzer. Well-ordering proofs for Martin-Löf type theory. Annals of pure and applied logic, vol. 92 (1998), pp. 113–159. » Bulletin of Symbolic Logic 6, no 4 (décembre 2000) : 478–79. http://dx.doi.org/10.2307/420979.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
32

Howard, W. A. « Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.) Studies in proof theory. Bibliopolis, Naples1984, ix + 91 pp. » Journal of Symbolic Logic 51, no 4 (décembre 1986) : 1075–76. http://dx.doi.org/10.2307/2273925.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
33

Möllerfeld, Michael. « Michael Rathjen. The superjump in Martin-Löf type theory. Logic Colloquium '98, Proceedings of the annual European summer meeting of the Association for Symbolic Logic, held in Prague, Czech Republic, August 9–15, 1998, edited by Samuel R. Buss, Petr Hájek, and Pavel Pudlák, Lecture notes in logic, no. 13, Association for Symbolic Logic, Urbana, and A K Peters, Natick, Mass., 2000, pp. 363–386. » Bulletin of Symbolic Logic 8, no 4 (décembre 2002) : 538. http://dx.doi.org/10.2178/bsl/1182353932.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
34

Klev, Ansten. « Identity in Martin‐Löf type theory ». Philosophy Compass 17, no 2 (28 décembre 2021). http://dx.doi.org/10.1111/phc3.12805.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
35

CLAIRAMBAULT, PIERRE, et PETER DYBJER. « The biequivalence of locally cartesian closed categories and Martin-Löf type theories ». Mathematical Structures in Computer Science 24, no 6 (29 avril 2014). http://dx.doi.org/10.1017/s0960129513000881.

Texte intégral
Résumé :
Seely's paper Locally cartesian closed categories and type theory (Seely 1984) contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Bénabou–Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development, we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result, we prove that if we remove Π-types, the resulting categories with families with only Σ and extensional identity types are biequivalent to left exact categories.
Styles APA, Harvard, Vancouver, ISO, etc.
36

Setzer, Anton. « Proof Theory of Martin-Löf Type Theory. An overview ». Mathématiques et sciences humaines, no 165 (1 mars 2004). http://dx.doi.org/10.4000/msh.2959.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
37

Wallet, Guy. « Choice sequence and nonstandard extension of type theory ». Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées Volume 20 - 2015 - Special... (17 septembre 2015). http://dx.doi.org/10.46298/arima.1995.

Texte intégral
Résumé :
International audience Partant de son travail Mathematics of Infinity (1989), Martin-Löf a développé l'idée d'un lien conceptuel profond entre les notions de suite de choix et d'objet mathématique nonstandard. Précisément, il a défini une extension nonstandard de la théorie des types en ajoutant une série d'axiomes nonstandard conçue comme une sorte de suite de choix. Enfin, dans une communication de 1999, il a présenté les grandes lignes d'une théorie des types nonstandard plus générale et munie d'un fort contenu computationnel. Le présent travail est une tentative de donner un développement complet d'une théorie de ce genre. Cependant, dans le but de garder un fort contrôle sur la théorie résultante et notablement pour éviter quelques problèmes en rapport avec l'égalité définitionnelle, le champ des axiomes nonstandard est moins général que ceux proposés dans sa communication de 1999. L'étude présente est poussée jusqu'à l' introduction d'une notion de proposition externe qui joue le même rôle que les propriétés externes si utiles dans l'analyse nonstandard usuelle. Du fait que ce texte débute par une introduction à la théorie des types de Martin-Löf, il peut intéresser les mathématiciens non familiers avec ce sujet.
Styles APA, Harvard, Vancouver, ISO, etc.
38

GAMBINO, NICOLA, et MARCO FEDERICO LARREA. « MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS ». Journal of Symbolic Logic, 8 juin 2021, 1–45. http://dx.doi.org/10.1017/jsl.2021.39.

Texte intégral
Styles APA, Harvard, Vancouver, ISO, etc.
39

ABEL, ANDREAS, JESPER COCKX, DOMINIQUE DEVRIESE, AMIN TIMANY et PHILIP WADLER. « Leibniz equality is isomorphic to Martin-Löf identity, parametrically ». Journal of Functional Programming 30 (2020). http://dx.doi.org/10.1017/s0956796820000155.

Texte intégral
Résumé :
Abstract Consider two widely used definitions of equality. That of Leibniz: one value equals another if any predicate that holds of the first holds of the second. And that of Martin-Löf: the type identifying one value with another is occupied if the two values are identical. The former dates back several centuries, while the latter is widely used in proof systems such as Agda and Coq. Here we show that the two definitions are isomorphic: we can convert any proof of Leibniz equality to one of Martin-Löf identity and vice versa, and each conversion followed by the other is the identity. One direction of the isomorphism depends crucially on values of the type corresponding to Leibniz equality satisfying functional extensionality and Reynolds’ notion of parametricity. The existence of the conversions is widely known (meaning that if one can prove one equality then one can prove the other), but that the two conversions form an isomorphism (internally) in the presence of parametricity and functional extensionality is, we believe, new. Our result is a special case of a more general relation that holds between inductive families and their Church encodings. Our proofs are given inside type theory, rather than meta-theoretically. Our paper is a literate Agda script.
Styles APA, Harvard, Vancouver, ISO, etc.
40

ANGIULI, CARLO, EDWARD MOREHOUSE, DANIEL R. LICATA et ROBERT HARPER. « Homotopical patch theory ». Journal of Functional Programming 26 (2016). http://dx.doi.org/10.1017/s0956796816000198.

Texte intégral
Résumé :
AbstractHomotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.
Styles APA, Harvard, Vancouver, ISO, etc.
41

Emmenegger, Jacopo, Fabio Pasquali et Giuseppe Rosolini. « Elementary fibrations of enriched groupoids ». Mathematical Structures in Computer Science, 19 novembre 2021, 1–21. http://dx.doi.org/10.1017/s096012952100030x.

Texte intégral
Résumé :
Abstract The present paper aims at stressing the importance of the Hofmann–Streicher groupoid model for Martin Löf Type Theory as a link with the first-order equality and its semantics via adjunctions. The groupoid model was introduced by Martin Hofmann in his Ph.D. thesis and later analysed in collaboration with Thomas Streicher. In this paper, after describing an algebraic weak factorisation system $$\mathsf {L, R}$$ on the category $${\cal C}-{\cal Gpd}$$ of $${\cal C}$$ -enriched groupoids, we prove that its fibration of algebras is elementary (in the sense of Lawvere) and use this fact to produce the factorisation of diagonals for $$\mathsf {L, R}$$ needed to interpret identity types.
Styles APA, Harvard, Vancouver, ISO, etc.
42

Petrakis, Iosif. « Proof-relevance in Bishop-style constructive mathematics ». Mathematical Structures in Computer Science, 31 mai 2022, 1–43. http://dx.doi.org/10.1017/s0960129522000159.

Texte intégral
Résumé :
Abstract Bishop’s presentation of his informal system of constructive mathematics BISH was on purpose closer to the proof-irrelevance of classical mathematics, although a form of proof-relevance was evident in the use of several notions of moduli (of convergence, of uniform continuity, of uniform differentiability, etc.). Focusing on membership and equality conditions for sets given by appropriate existential formulas, we define certain families of proof sets that provide a BHK-interpretation of formulas that correspond to the standard atomic formulas of a first-order theory, within Bishop set theory $(\mathrm{BST})$ , our minimal extension of Bishop’s theory of sets. With the machinery of the general theory of families of sets, this BHK-interpretation within BST is extended to complex formulas. Consequently, we can associate to many formulas $\phi$ of BISH a set ${\texttt{Prf}}(\phi)$ of “proofs” or witnesses of $\phi$ . Abstracting from several examples of totalities in BISH, we define the notion of a set with a proof-relevant equality, and of a Martin-Löf set, a special case of the former, the equality of which corresponds to the identity type of a type in intensional Martin-Löf type theory $(\mathrm{MLTT})$ . Through the concepts and results of BST notions and facts of MLTT and its extensions (either with the axiom of function extensionality or with Vooevodsky’s axiom of univalence) can be translated into BISH. While Bishop’s theory of sets is standardly understood through its translation to MLTT, our development of BST offers a partial translation in the converse direction.
Styles APA, Harvard, Vancouver, ISO, etc.
43

UUSTALU, TARMO, et NICCOLÒ VELTRI. « Finiteness and rational sequences, constructively ». Journal of Functional Programming 27 (2017). http://dx.doi.org/10.1017/s0956796817000041.

Texte intégral
Résumé :
AbstractRational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.
Styles APA, Harvard, Vancouver, ISO, etc.
44

Bezem, Marc, Thierry Coquand, Peter Dybjer et Martín Escardó. « On generalized algebraic theories and categories with families ». Mathematical Structures in Computer Science, 18 octobre 2021, 1–18. http://dx.doi.org/10.1017/s0960129521000268.

Texte intégral
Résumé :
Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.
Styles APA, Harvard, Vancouver, ISO, etc.
Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!

Vers la bibliographie