Skip to content

Modern Perspective on Type Theory From Its Origins until Today

Spend $50 to get a free movie!

ISBN-10: 1402023340

ISBN-13: 9781402023347

Edition: 2005

Authors: Fairouz Kamareddine, Twan Laan, Rob Nederpelt

List price: $199.99
Blue ribbon 30 day, 100% satisfaction guarantee!
Out of stock
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!

Customers also bought

Book details

List price: $199.99
Copyright year: 2005
Publisher: Springer Netherlands
Publication date: 6/9/2004
Binding: Hardcover
Pages: 360
Size: 6.25" wide x 9.50" long x 0.75" tall
Weight: 1.584
Language: English

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