An Overview of Type Theories
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605475121 | ||
| 003 | CHVBK | ||
| 005 | 20210128100350.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150301xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s10516-014-9260-9 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s10516-014-9260-9 | ||
| 100 | 1 | |a Guallart |D Nino |u Universidad de Santiago de Compostela, Santiago de Compostela, Spain |4 aut | |
| 245 | 1 | 3 | |a An Overview of Type Theories |h [Elektronische Daten] |c [Nino Guallart] |
| 520 | 3 | |a Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an active role in the development of computational science and core mathematics. It is worth exploring some of them in depth, particularly predicative Martin-Löf's intuitionistic type theory and impredicative Coquand's calculus of constructions. The logical and philosophical differences and similarities between them will be studied, showing the relationship between these type theories and other fields of logic. | |
| 540 | |a Springer Science+Business Media Dordrecht, 2014 | ||
| 690 | 7 | |a Higher-order logic |2 nationallicence | |
| 690 | 7 | |a Type theory |2 nationallicence | |
| 690 | 7 | |a Intuitionistic logic |2 nationallicence | |
| 690 | 7 | |a Lambda calculus |2 nationallicence | |
| 690 | 7 | |a Foundations of mathematics |2 nationallicence | |
| 773 | 0 | |t Axiomathes |d Springer Netherlands |g 25/1(2015-03-01), 61-77 |x 1122-1151 |q 25:1<61 |1 2015 |2 25 |o 10516 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s10516-014-9260-9 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s10516-014-9260-9 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 100 |E 1- |a Guallart |D Nino |u Universidad de Santiago de Compostela, Santiago de Compostela, Spain |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Axiomathes |d Springer Netherlands |g 25/1(2015-03-01), 61-77 |x 1122-1151 |q 25:1<61 |1 2015 |2 25 |o 10516 | ||