A Modern Perspective on Type Theory: From its Origins until Today

Description

This book provides an overview of type theory. The first part of the book is historical, yet at the same time, places historical systems in the modern setting. The second part deals with modern type theory as it developed since the 1940s, and with the role of propositions as types (or proofs as terms. The third part proposes new systems that bring more advantages together. Contents......Page 6 Part I......Page 12 Part II......Page 14 Part III......Page 15 Acknowledgements......Page 16 Avoiding the paradox in set theory......Page 18 Avoiding the paradox in type theory......Page 21 The approach......Page 22 I: The Evolution of Type Theory until the 1940s......Page 24 1 Prehistory......Page 26 1a: Paradox threats......Page 27 1b: Paradox threats in formal systems......Page 28 2 Type theory in Principia Mathematica......Page 36 2a: Principia’s propositional functions......Page 39 2b: The Ramified Theory of Types RTT......Page 52 2c: Properties of RTT......Page 66 2d: Legal propositional functions......Page 76 Conclusions......Page 82 3 Deramification......Page 86 3a: History of the deramification......Page 87 3b: The Simple Theory of Types STT......Page 93 3c: Are orders to be blamed?......Page 98 Conclusions......Page 117 II: Propositions as Types, Pure Type Systems, AUTOMATH......Page 120 4 Propositions as Types and Pure Type Systems......Page 122 4a: Propositions as Types and Proofs as Terms (PAT)......Page 123 4b: Lambda calculus......Page 129 4c: Pure Type Systems......Page 133 5a: RTT in PAT style......Page 142 5b: STT in PAT style......Page 167 Conclusions......Page 168 6 A Correspondence between RTT and the system Nuprl......Page 170 6a: On the role of orders......Page 171 6b: The Nuprl type system......Page 173 6c: RTT in Nuprl......Page 185 Conclusions......Page 190 7 Automath......Page 196 7a: Description of AUTOMATH......Page 199 7b; From AUT-68 towards a PTS......Page 211 7c: λ68......Page 217 7d: More Suitable Pure Type Systems for AUTOMATH......Page 240 Conclusions......Page 246 III: Extensions of Pure Type Systems......Page 248 8 Pure Type Systems with definitions......Page 250 8a: Definitions in contexts......Page 251 8b: Definitions in the terms and the contexts......Page 255 Conclusions......Page 257 9 The Barendregt cube with parameters......Page 260 9a: On parameters in the Barendregt cube......Page 261 9b: The Barendregt cube refined with parameters......Page 267 Conclusions......Page 270 10 Pure Type Systems with parameters and definitions......Page 272 10a: Parametric constants and definitions......Page 273 10b: Properties of terms......Page 287 10c: Properties of legal terms......Page 298 10d: Restrictive use of parameters......Page 307 10e: Systems in the refined Barendregt cube......Page 315 10f: First-order predicate logic......Page 320 Conclusions: Yet another extension of PTSs?......Page 324 Aa: Pure Type Systems......Page 328 Ab: The Barendregt cube......Page 329 Ac: The Ramified Theory of Types......Page 331 Ad: The Simple Theory of Types......Page 335 Ae: Church’s simply typed λ-calculus λ[sub(→Church)]......Page 338 Af: A fragment of Nuprl in PTS-style......Page 339 Ag: AUTOMATH......Page 341 Ah: Pure Type Systems with definitions......Page 345 Ai: Pure Type Systems with parametric constants......Page 349 Aj: A CD-PTS and its subsystems......Page 350 Bibliography......Page 354 C......Page 366 F......Page 367 L......Page 368 P......Page 369 S......Page 370 W......Page 371 R......Page 372 Z......Page 373 List of Figures......Page 374