| |
| |
| Preface | |
| |
| |
| Preliminaries | |
| |
| |
| Overview of this book | |
| |
| |
| Acknowledgements | |
| |
| |
| Introduction the Evolution of Type Theory until the 1940s | |
| |
| |
| |
| Prehistory | |
| |
| |
| |
| Paradox threats | |
| |
| |
| |
| Paradox threats in formal systems | |
| |
| |
| |
| Type theory in Pricipia Mathematica | |
| |
| |
| |
| Principia's propositional functions | |
| |
| |
| |
| The Ramified Theory of Types RTT | |
| |
| |
| |
| Properties of RTT | |
| |
| |
| |
| Legal propositional functions | |
| |
| |
| Conclusions | |
| |
| |
| |
| Deramification | |
| |
| |
| |
| History of the deramification | |
| |
| |
| |
| The Simple Theory of Types STT | |
| |
| |
| |
| Are orders to be blamed? | |
| |
| |
| Conclusions | |
| |
| |
| |
| Propositions as Types, Pure Type Systems, AUTOMATH | |
| |
| |
| |
| Propositions as Types and Pure Type Systems | |
| |
| |
| |
| Propositions as types and proofs as terms (PAT) | |
| |
| |
| |
| Lambda calculus | |
| |
| |
| |
| Pure type systems | |
| |
| |
| |
| The pre-PAT and STT in PAT-style | |
| |
| |
| |
| RTT in PAT-style | |
| |
| |
| |
| STT in PAT-style | |
| |
| |
| |
| A correspondence between RTT and the system Nuprl | |
| |
| |
| |
| On the role of orders | |
| |
| |
| |
| The Nuprl type system | |
| |
| |
| |
| RTT in Nuprl | |
| |
| |
| Conclusions | |
| |
| |
| |
| Automath | |
| |
| |
| |
| Description of AUTOMATH | |
| |
| |
| |
| From AUT-68 towards a PTS | |
| |
| |
| |
| lambda68 | |
| |
| |
| |
| More suitable pure type systems for AUTOMATH | |
| |
| |
| Conclusions | |
| |
| |
| |
| Extensions of Pure Type Systems | |
| |
| |
| |
| Pure type systems with definitions | |
| |
| |
| |
| Definitions in contexts | |
| |
| |
| |
| Definitions in the terms and the contexts | |
| |
| |
| |
| The Barendregt cube with parameters | |
| |
| |
| |
| On parameters in the Barendregt cube | |
| |
| |
| |
| The Barendregt cube refined with parameters | |
| |
| |
| |
| Pure Type Systems with parameters and definitions | |
| |
| |
| |
| Parametric constraints and definitions | |
| |
| |
| |
| Properties of terms | |
| |
| |
| |
| Properties of legal terms | |
| |
| |
| |
| Restrictive use of parameters | |
| |
| |
| |
| Systems in the redefined Barendregt cube | |
| |
| |
| |
| First-order predicate logic | |
| |
| |
| Conclusions: yet another extension of PTSs? | |
| |
| |
| Practical motivation | |
| |
| |
| The heart of type theory | |
| |
| |
| Future work. A: Type Systems in this Book | |
| |
| |
| |
| Pure Type Systems | |
| |
| |
| |
| The Barendregt cube | |
| |
| |
| |
| The Ramified Theory of Types | |
| |
| |
| |
| The Simple Theory of Types | |
| |
| |
| |
| Church's simply typed lambda-calculus lambda Church. A.f | |
| |
| |
| A fragment of Nuprl in PTS-style | |
| |
| |
| |
| Automath | |
| |
| |
| |
| Pure Type Systems with definitions | |
| |
| |
| |
| Pure Type Systems with parametric constants | |
| |
| |
| |
| A CD-PTS and its subsystems | |
| |
| |
| Bibliography | |
| |
| |
| Subject | |
| |
| |
| Index | |
| |
| |
| Name Index | |
| |
| |
| List of Figures | |