Volume 7: January - December 1997

Issue 2: 1997

Abstract


Reading between the lines in constructive type theory

  • Reading between the lines in constructive type theory
  • R. Turner

    Department of Computer Science, University of Essex, Wivenhoe Park, Colchester, Essex, CO4 3SQ, UK

    ABSTRACT

    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

    Pages: 229 - 250

    Part of the OUP Journal of Logic and Computation WWW service


    General Information

    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.