Now showing items 5-7 of 7

    • A Non-Type-Theoretic Definition of Martin-Lof's Types 

      Allen, Stuart (Cornell University, 1987-04)
      It is possible to make a natural non-type-theoretic reinterpretation of Martin-Lof's type theory. This paper presents an inductive definition of the types explicitly defined in Martin-Lof's paper, Constructive Mathematics ...
    • A Non-Type-Theoretic Semantics For Type-Theoretic Language 

      Allen, Stuart (Cornell University, 1987-09)
      Since 1970 several methods have been proposed for using formal systems of constructive logic as programming languages. One prominent approach is based upon systems of computationally significant terms which either bear ...
    • A Notation for Computer Aided Mathematics 

      Mannion, Conal; Allen, Stuart (Cornell University, 1994-02)
      The NuPrl4 term structure and editor display mechanism are used to provide unambiguous notations for use in the the development of computer supported mathematical arguments. These notations are used to provide a natural ...