Now showing items 1-7 of 7

    • Automating Reasoning in an Implementation of Constructive Type Theory 

      Howe, Douglas J. (Cornell University, 1988-06)
      The starting point for this thesis is the Nuprl proof development system. Nuprl is an environment for the development of formal computational mathematics and has a rich constructive type theory as a logical basis. It ...
    • The Computational Behaviour of Girard's Paradox 

      Howe, Douglas J. (Cornell University, 1987-03)
      In their paper "Type" Is Not a Type, Meyer and Reinhold argued that serious pathologies can result when a type of all types is added to a programing language with dependent types. Central to their argument is the claim ...
    • Computational Metatheory in Nuprl 

      Howe, Douglas J. (Cornell University, 1988-03)
      This paper describes an implementation within Nuprl of mechanisms that support the use of Nuprl's type theory as a language for constructing theorem-provind procedures. The main componenet of the implementation is a ...
    • Implementing Metamathematics as an Approach to Automatic Theorem Proving 

      Constable, Robert L.; Howe, Douglas J. (Cornell University, 1989-04)
      A simple but important algorithm used to support automated reasoning is called matching: given two terms it produces a substitution, if one exists, that maps the first term to the second. In this paper the matching ...
    • Implementing Number Theory: An Experiment with Nuprl 

      Howe, Douglas J. (Cornell University, 1986-05)
      We describe the results of an experiment in which the Nuprl proof development system was used in conjunction with a collection of simple proof-assisting programs to constructively prove a substantial theorem of number ...
    • Impredicative Strong Existential Equivalent to Type:Type 

      Hook, James G.; Howe, Douglas J. (Cornell University, 1986-06)
    • Nuprl as a General Logic 

      Constable, Robert L.; Howe, Douglas J. (Cornell University, 1989-06)
      Study of the architecture and design of proof development systems has become important lately as their use has spread and become closely tied to programming environments. One of the central issues is how to provide a ...