Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

Implementing Number Theory: An Experiment with Nuprl. - Douglas J. Howe (CADE, 1986)

The Computational Behaviour of Girard's Paradox - Douglas J. Howe (LICS, 1987)

Automating Reasoning in an Implementation of Constructive Type Theory. - Douglas J. Howe (1987)

Computational Metatheory in Nuprl. - Douglas J. Howe (CADE, 1988)

Equality In Lazy Computation Systems - Douglas J. Howe (LICS, 1989)

The Semantics of Reflected Proof - Stuart F. Allen; Robert L. Constable; Douglas J. Howe; William E. Aitken (LICS, 1990)

Implementing Constructive Real Analysis: Preliminary Report. - Jawahar Chirimar; Douglas J. Howe (Constructivity in Computer Science, 1991)

On Computational Open-Endedness in Martin-Löf's Type Theory - Douglas J. Howe (LICS, 1991)

Some Normalization Properties of Martin-Löf's Type Theory, and Applications. - David A. Basin; Douglas J. Howe (TACS, 1991)

Reasoning About Functional Programs in Nuprl. - Douglas J. Howe (Functional Programming, Concurrency, Simulation and Automated Reasoning, 1993)

Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. - Amy P. Felty; Douglas J. Howe (CADE, 1994)

Generalization and Reuse of Tactic Proofs. - Amy P. Felty; Douglas J. Howe (LPAR, 1994)

An Operational Approach to Combining Classical Set Theory and Functional Programming Languages. - Douglas J. Howe; Scott D. Stoller (TACS, 1994)

Semantic Foundations for Embedding HOL in Nuprl. - Douglas J. Howe (AMAST, 1996)

Importing Mathematics from HOL into Nuprl. - Douglas J. Howe (TPHOLs, 1996)

Proving Congruence of Bisimulation in Functional Programming Languages. - Douglas J. Howe (Inf. Comput., 1996)

Hybrid Interactive Theorem Proving Using Nuprl and HOL. - Amy P. Felty; Douglas J. Howe (CADE, 1997)

Protocol Verification in Nuprl. - Amy P. Felty; Douglas J. Howe; Frank A. Stomp (CAV, 1998)

Toward Sharing Libraries of Mathematics between Theorem Provers. - Douglas J. Howe (FroCoS, 1998)

A Type Annotation Scheme for Nuprl. - Douglas J. Howe (TPHOLs, 1998)

Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. - Amy P. Felty; Douglas J. Howe; Abhik Roychoudhury (CADE, 1999)

Interactive Theorem Proving Using Type Theory. - Douglas J. Howe (CSL, 1999)

Electricity Deregulation: It's New Bonanza. - Douglas J. Howe; James E. Cuccaro (Inf. Syst. Manag., 2001)

An approach to formal verication of real time concurrent Ada programs. - Douglas J. Howe; Stephen Michell (IRTAW, 2003)

Higher-order abstract syntax in classical higher-order logic. - Douglas J. Howe (LFMTP, 2009)

Higher-Order Abstract Syntax in Isabelle/HOL. - Douglas J. Howe (ITP, 2010)