Douglas J. Howe

27 papers A* 5A 5B 3Journal 2Unranked 10

Year	Rank	Type	Title / Venue / Authors
2010	B	`conf`	Higher-Order Abstract Syntax in Isabelle/HOL. ITP Douglas J. Howe
2009	—	`conf`	Higher-order abstract syntax in classical higher-order logic. LFMTP Douglas J. Howe
2003	—	`conf`	An approach to formal verication of real time concurrent Ada programs. IRTAW Douglas J. Howe, Stephen Michell
2001	J	`jnl`	Electricity Deregulation: It's New Bonanza. Inf. Syst. Manag. Douglas J. Howe, James E. Cuccaro
1999	A	`conf`	Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. CADE Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury
1999	B	`conf`	Interactive Theorem Proving Using Type Theory. CSL Douglas J. Howe
1998	—	`conf`	A Type Annotation Scheme for Nuprl. TPHOLs Douglas J. Howe
1998	A*	`conf`	Protocol Verification in Nuprl. CAV Amy P. Felty, Douglas J. Howe, Frank A. Stomp
1998	—	`conf`	Toward Sharing Libraries of Mathematics between Theorem Provers. FroCoS Douglas J. Howe
1997	A	`conf`	Hybrid Interactive Theorem Proving Using Nuprl and HOL. CADE Amy P. Felty, Douglas J. Howe
1996	—	`conf`	Importing Mathematics from HOL into Nuprl. TPHOLs Douglas J. Howe
1996	J	`jnl`	Proving Congruence of Bisimulation in Functional Programming Languages. Inf. Comput. Douglas J. Howe
1996	—	`conf`	Semantic Foundations for Embedding HOL in Nuprl. AMAST Douglas J. Howe
1994	—	`conf`	An Operational Approach to Combining Classical Set Theory and Functional Programming Languages. TACS Douglas J. Howe, Scott D. Stoller
1994	B	`conf`	Generalization and Reuse of Tactic Proofs. LPAR Amy P. Felty, Douglas J. Howe
1994	A	`conf`	Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables. CADE Amy P. Felty, Douglas J. Howe
1993	—	`conf`	Reasoning About Functional Programs in Nuprl. Functional Programming, Concurrency, Simulation and Automated Reasoning Douglas J. Howe
1991	—	`conf`	Implementing Constructive Real Analysis: Preliminary Report. Constructivity in Computer Science Jawahar Chirimar, Douglas J. Howe
1991	A*	`conf`	On Computational Open-Endedness in Martin-Löf's Type Theory LICS Douglas J. Howe
1991	—	`conf`	Some Normalization Properties of Martin-Löf's Type Theory, and Applications. TACS David A. Basin, Douglas J. Howe
1990	A*	`conf`	The Semantics of Reflected Proof LICS Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken
1989	A*	`conf`	Equality In Lazy Computation Systems LICS Douglas J. Howe
1988	A	`conf`	Computational Metatheory in Nuprl. CADE Douglas J. Howe
1987	—	`—`	Automating Reasoning in an Implementation of Constructive Type Theory. Douglas J. Howe
1987	A*	`conf`	The Computational Behaviour of Girard's Paradox LICS Douglas J. Howe
1986	A	`conf`	Implementing Number Theory: An Experiment with Nuprl. CADE Douglas J. Howe
1986	—	`book`	Implementing mathematics with the Nuprl proof development system. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith