This thesis presents a type system, Provability Calculus of
Constructions (PCoC) that can be used for the formalization of
logic. In a theorem prover based on the system, the user can
extend the prover with new inference rules in a logically
consistent manner. This is done by representing PCoC as values and
data types within PCoC. The new feature of PCoC is that results of
the representation of PCoC can be lifted to PCoC itself. The
lifting is fully formalized in PCoC, and the logic therefore
supports reflection.
| Publisher | IT-DTU |
|---|
| Number of pages | 213 |
|---|
| Publication status | Published - 1999 |
|---|