CMU-CS-98-164Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-98-164
Karl Crary October 1998
CMU-CS-98-164.ps
Keywords: Admissibility, fixpoint induction, partial functions,
type theory
In this paper I present two new tools, predicate-admissibility and monotonicity, for showing types to be admissible. These tools show a wide class of types to be admissible; in particular, they show many dependent products to be admissible. This alleviates difficulties in applying partial types to theorem proving in practice. I also present a general least upper bound theorem for fixed points with regard to a computational approximation relation, and show an elegant application of the theorem to compactness. 27 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |