Log in

Relevant bibliographies by topics / Martin-Löf Type Theory

Contents

Journal articles
Dissertations / Theses
Books
Book chapters
Conference papers

Academic literature on the topic 'Martin-Löf Type Theory'

Author: Grafiati

Published: 11 March 2023

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Martin-Löf Type Theory.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Martin-Löf Type Theory"

1

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

2

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

3

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

4

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

5

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

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 (1993): 63–92. http://dx.doi.org/10.1017/s0960129500000128.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

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 (1991): 1012–15. http://dx.doi.org/10.2307/2275068.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

8

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic "Martin-Löf Type Theory"

1

Girardi, Marco. "Proof theoretical issues in Martin-Löf Type Theory and Homotopy Type Theory." Doctoral thesis, Università degli studi di Trento, 2022. http://hdl.handle.net/11572/348681.

Full text

Abstract:

Homotopy Type Theory (HoTT) is a quite recent branch of research in mathematical logic, which provides interesting connections among various areas of mathematics. It was first introduced by Vladimir Voevodsky as a means to develop synthetic homotopy theory, and further advancements suggested that it can be used as a formal foundation to mathematics. Among its notable features, inductive and higher inductive types are of great interest, e.g. allowing for the study of geometric entities (such as spheres) in the setting of HoTT. However, so far in most of the literature higher inductive types are treated in an ad-hoc way; there is no easy general schema stating what an higher inductive type is, thus hindering the study of the related proof theory. Moreover, although Martin-Löf Type Theory has been deeply and widely studied, many proof theoretic results about its specific variant used in HoTT are folklore, and the proofs are missing. In this final talk, we provide an overview on some results we obtained, aiming to address these problems. In the first part of the talk, we will discuss a normalization theorem for the type theory underlying HoTT. In the second part of the talk we will propose a general syntax schema to encapsulate a relevant class of higher inductive types, potentially allowing for future study of the proof theory of HoTT enriched with such types.

APA, Harvard, Vancouver, ISO, and other styles

2

Fors, Mikael. "Elementary Discrete Sets in Martin-Löf Type Theory." Thesis, Uppsala universitet, Algebra och geometri, 2012. http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-175717.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Mundim, Bruno Rigonato. "Uma abordagem sobre a concepção de proposição da teoria institucionalista de tipos." Universidade Federal de Goiás, 2013. http://repositorio.bc.ufg.br/tede/handle/tede/3337.

Full text

Abstract:

Submitted by Erika Demachki (erikademachki@gmail.com) on 2014-10-13T19:12:35Z No. of bitstreams: 2 Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5)<br>Approved for entry into archive by Jaqueline Silva (jtas29@gmail.com) on 2014-10-13T20:49:48Z (GMT) No. of bitstreams: 2 Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5)<br>Made available in DSpace on 2014-10-13T20:49:48Z (GMT). No. of bitstreams: 2 Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2013-09-02<br>Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES<br>By means of the Curry-Howard Correspondence Martin-Löf’s intuitionistic type theory claims that to define a proposition by laying down how its canonical proofs are formed is the same as to define a set by laying down how its canonical elements are formed; consequently a proposition can be seen as the set of its proofs. On the other hand, we find in this very same theory a distinction between the notions of set and of type, such that the difference of the latter in relation to the former consists in the fact that to form a type we do not need to present an exhaustive prescription for the formation of its objects; it is sufficient to just have a general notion of what would be an arbitrary object that inhabits such type. Thus we argue that we can extract two distinct notions of propositon from the intuitionistic type theory, one which treats propositions as types and another which treats propositions as sets. Such distinction will have some bearing on discussions concerning hypothetical demonstrations and conjecture’s formation.<br>A teoria intuicionista de tipos, de Martin-Löf, alega, à luz da correspondência Curry- Howard, que definir uma proposição por meio do estabelecimento de como as suas provas canônicas são formadas é o mesmo que definir um conjunto por meio do estabelecimento de como os seus elementos canônicos são formados, fazendo com que uma proposição possa ser vista como o conjunto de suas provas. Por outro lado, encontramos nessa mesma teoria uma distinção entre as noções de conjunto e tipo, sendo que a diferença deste em relação àquele consiste no fato de que para se formar um tipo não é preciso apresentar uma prescrição exaustiva da formação de seus objetos, basta se ter uma noção geral do que seria um objeto arbitrário que o habita. Tendo isso em conta, argumentamos que podemos extrair da teoria intuicionista de tipos duas concepções de proposição distintas, uma que considera proposições como tipos e outra que considera proposições como conjuntos. Tal distinção implicará em algumas considerações envolvendo questões sobre demonstrações hipotéticas e a formação de conjecturas.

APA, Harvard, Vancouver, ISO, and other styles

Books on the topic "Martin-Löf Type Theory"

1

Sambin, Giovanni, and Jan M. Smith. Twenty Five Years of Constructive Type Theory. Oxford University Press, 1998. http://dx.doi.org/10.1093/oso/9780198501275.001.0001.

Full text

Abstract:

Per Martin-Löf's work on the development of constructive type theory has had a tremendous impact on the fields of logic and the foundations of mathematics. It also has broader philosophical significance and important applications in areas such as computing science and linguistics. This volume draws together contributions from researchers whose work builds on the theory developed by Martin-Löf over the last twenty-five years. As well as celebrating the anniversary of the birth of the subject it covers many of the diverse fields which are now influenced by type theory. It is an invaluable record of current activity and includes contributions from N. G. de Bruijn and William Tait, both important figures in the early development of the subject. Also published for the first time is one of Per Martin-Löf's earliest papers.

APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Martin-Löf Type Theory"

1

Setzer, Anton. "Proof theory and Martin-Löf Type Theory." In One Hundred Years of Intuitionism (1907–2007). Birkhäuser Basel, 2008. http://dx.doi.org/10.1007/978-3-7643-8653-5_16.

Full text

APA, Harvard, Vancouver, ISO, and other styles

2

Setzer, Anton. "Partial Recursive Functions in Martin-Löf Type Theory." In Logical Approaches to Computational Barriers. Springer Berlin Heidelberg, 2006. http://dx.doi.org/10.1007/11780342_51.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Hofmann, Martin. "Elimination of extensionality in Martin-Löf type theory." In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1994. http://dx.doi.org/10.1007/3-540-58085-9_76.

Full text

APA, Harvard, Vancouver, ISO, and other styles

4

Thompson, Simon. "Are subsets necessary in Martin-Löf type theory?" In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1992. http://dx.doi.org/10.1007/bfb0021082.

Full text

APA, Harvard, Vancouver, ISO, and other styles

5

De Marchi, Federico. "On the Semantics of Coinductive Types in Martin-Löf Type Theory." In Algebra and Coalgebra in Computer Science. Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/11548133_8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

6

Rathjen, Michael. "The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory." In Logicism, Intuitionism, and Formalism. Springer Netherlands, 2009. http://dx.doi.org/10.1007/978-1-4020-8926-8_17.

Full text

APA, Harvard, Vancouver, ISO, and other styles

7

Fridlender, Daniel, and Miguel Pagano. "A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation." In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2013. http://dx.doi.org/10.1007/978-3-642-38946-7_12.

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

Setzer, A. "An Upper Bound for the Proof-Theoretic Strength of Martin-Löf Type Theory with W-type and One Universe." In The Legacy of Kurt Schütte. Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-49424-7_16.

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

Altenkirch, Thorsten, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. "Constructing a universe for the setoid model." In Lecture Notes in Computer Science. Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-71995-1_1.

Full text

Abstract:

AbstractThe setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-Löf type theory with constructs that give full access to the extensionality principles that hold in the setoid model.Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.

APA, Harvard, Vancouver, ISO, and other styles

10

Nördstrom, B., and K. Petersson. "Martin-Löf ’s type theory." In Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures. Oxford University Press, 2001. http://dx.doi.org/10.1093/oso/9780198537816.003.0004.

Full text

Abstract:

The type theory described in this chapter has been developed by Martin-Löf with the original aim of being a clarification of constructive mathematics. Unlike most other formalizations of mathematics, type theory is not based on predicate logic. Instead, the logical constants are interpreted within type theory through the Curry-Howard correspondence between propositions and sets [Curry and Feys, 1958; Howard, 1980]: a proposition is interpreted as a set whose elements represent the proofs of the proposition. It is also possible to view a set as a problem description in a way similar to Kolmogorov’s explanation of the intuitionistic propositional calculus [Kolmogorov, 1932]. In particular, a set can be seen as a specification of a programming problem; the elements of the set are then the programs that satisfy the specification. An advantage of using type theory for program construction is that it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. As a programming language, type theory is similar to typed functional languages such as ML [Gordon et al., 1979; Milner et al., 1990] and Haskell [Hudak et al, 1992], but a major difference is that the evaluation of a well-typed program always terminates. The notion of constructive proof is closely related to the notion of computer program. To prove a proposition ("x Î A)($yÎB)P(x,y) constructively means to give a function f which when applied to an element a in A gives an element b in B such that P(a, b) holds. So if the proposition ("xÎ A)($yÎB)P(x,y) expresses a specification, then the function f obtained from the proof is a program satisfying the specification. A constructive proof could therefore itself be seen as a computer program and the process of computing the value of a program corresponds to the process of normalizing a proof. It is by this computational content of a constructive proof that type theory can be used as a programming language; and since the program is obtained from a proof of its specification, type theory can be used as a programming logic.

APA, Harvard, Vancouver, ISO, and other styles

Conference papers on the topic "Martin-Löf Type Theory"

1

Abel, Andreas, Thierry Coquand, and Peter Dybjer. "Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements." In 2007 22nd Annual IEEE Symposium on Logic in Computer Science. IEEE, 2007. http://dx.doi.org/10.1109/lics.2007.33.

Full text

APA, Harvard, Vancouver, ISO, and other styles

2

Wieczorek, Paweł, and Dariusz Biernacki. "A Coq formalization of normalization by evaluation for Martin-Löf type theory." In CPP '18: Certified Proofs and Programs. ACM, 2018. http://dx.doi.org/10.1145/3167091.

Full text

APA, Harvard, Vancouver, ISO, and other styles

3

Wieczorek, Paweł, and Dariusz Biernacki. "A Coq formalization of normalization by evaluation for Martin-Löf type theory." In the 7th ACM SIGPLAN International Conference. ACM Press, 2018. http://dx.doi.org/10.1145/3176245.3167091.

Full text

APA, Harvard, Vancouver, ISO, and other styles

We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!