Constructions, inductive types and strong normalization
This thesis contains an investigation of Coquand's Calculus of Construction, a basic impredicative Type Theory. We review syntactic properties of the calculus, in particular decidability of equality and type-checking, based on the equality-as-judgement presentation. We present a set-theoretic n...
| Main Author: | |
|---|---|
| Published: |
University of Edinburgh
1993
|
| Subjects: | |
| Online Access: | http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.640438 |