Next:
Introduction
Up:
Typed Logic
Previous:
Heyting's semantics
Type theory
type theory
Introduction
Essential features
Language and logic
Level restrictions
Architecture of type theory
Inference mechanism
Functions
Duality and disjoint unions
Inductive type classes and large types
Dependent types
Universes
Using type systems to model type theories
Modeling hypothetical judgments
A semantics of proofs
Curry-Howard isomorphism
Sequents to typing judgments
Expressing well-formedness of formulas
Proofs as programs
Refinement style programming
Explicit programming style
James Wallis
1999-09-17
