caa a22 4500 605475121 CHVBK 20210128100350.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s10516-014-9260-9 doi (NATIONALLICENCE)springer-10.1007/s10516-014-9260-9 Guallart Nino Universidad de Santiago de Compostela, Santiago de Compostela, Spain aut An Overview of Type Theories [Elektronische Daten] [Nino Guallart] 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. Springer Science+Business Media Dordrecht, 2014 Higher-order logic nationallicence Type theory nationallicence Intuitionistic logic nationallicence Lambda calculus nationallicence Foundations of mathematics nationallicence Axiomathes Springer Netherlands 25/1(2015-03-01), 61-77 1122-1151 25:1<61 2015 25 10516 https://doi.org/10.1007/s10516-014-9260-9 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s10516-014-9260-9 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Guallart Nino Universidad de Santiago de Compostela, Santiago de Compostela, Spain aut NATIONALLICENCE 773 0- Axiomathes Springer Netherlands 25/1(2015-03-01), 61-77 1122-1151 25:1<61 2015 25 10516