 There are different ways in which intuitionsitic logic can be automated. One is to directly implement the intuitionistic versions of Gentzen’s sequent and natural deduction calculi, LJ and NJ respectively. This approach inherits the stronger normalization results enjoyed by these calculi allowing for a more compact mechanization than their classical counterparts. Another approach at mechanizing intuitionistic logic is to exploit its semantic similarities with the modal logic S4 and piggy back on an automated implementation of S4. Automating intuitionistic logic has applications in software development since writing a program that meets a specification corresponds to the problem of proving the specification within an intuitionistic logic (Martin-Löf 1982). A system that automated the proof construction process would have important applications in algorithm design but also in constructive mathematics. Nuprl (Constable et al. 1986) is a computer system supporting a particular mathematical theory, namely constructive type theory, and whose aim is to provide assistance in the proof development process. The focus is on logic-based tools to support programming and on implementing formal computational mathematics. Over the years the scope of the Nuprl project has expanded from “proofs-as-programs” to “systems-as-theories”. Similar in spirit and based on the Curry-Howard isomorphism, the Coq system formalizes its proofs in the Calculus of Inductive Constructions, a λ-calculus with a rich system of types including dependent types (Coquand &amp; Huet 1988, Coquand &amp; Paulin-Mohring 1988). Like Nuprl, Coq is designed to assist in the development of mathematical proofs as well as computer programs from their formal specifications.