R. Turner Department of Computer Science, University of Essex, Wivenhoe Park, Colchester, Essex, CO4 3SQ, UK
We formulate and investigate various ways of (conservatively) extending Martin-Lof's type theories with separation types and choice principles and demonstrate how these extensions can be employed to formalise Bishop's mathematical practice of hiding and recovering witnessing information.
Keywords: Constructive mathematics, type theory, Bishop's mathematics
Part of the OUP Journal of Logic and Computation WWW service
Click here to register with OUP.
This page is maintained by OUP admin
Part of the OUP Journals World Wide Web service.
Last modification: 22 Jul 1997
Copyright© Oxford University Press, 1997.