John Harrison: Other People's Papers

Miscellaneous publications by other people that I have sometimes wanted to refer to (this does not constitute an endorsement).

Domain Theory. S. Abramsky and A. Jung.
A Study of User Activity in Interactive Theorem Proving. J. S. Aitken, P. Gray, T. Melham and M. Thomas.
Model Elimination without Contrapositives and its Application to PTTP. P. Baumgartner, U. Furbach.
Lean, Tableau-based Deduction. B. Beckert and J. Posegga.
On Understanding Types, Data Abstraction, and Polymorphism. Luca Cardelli and Peter Wegner.
Explicit Substitutions. Luca Cardelli.
Proof Accounts in HOL (DRAFT). Avra Cohn.
Completion Without Failure. Nachum Dershowitz.
Merging HOL with Set Theory: preliminary experiments. Mike Gordon.
Notes on PVS from a HOL perspective. Mike Gordon.
The Semantics of Types in Programming Languages. Carl Gunter.
Naive Set Theory with a Universal Set. Randall Holmes.
The Markgraf Karl Refutation Procedure. Hans Jürgen Ohlbach and Jörg H. Siekmann.
Outline of a proof theory of parametricity. Harry Mairson.
The Ignorance of Bourbaki. Adrian Mathias.
Logic and Terror. Adrian Mathias.
Notes on Mac Lane Set Theory. Adrian Mathias.
Mechanising Set Theory: Cardinal Arithmetic and the Axiom of Choice. Lawrence C. Paulson & Krzysztof Grabczewski.
Structural Cut Elimination. Frank Pfenning.
On Extensibility of Proof Checkers. Randy Pollack.
An Overview of the Mizar project. Piotr Rudnicki.
DELTA --- A Bottom-up Preprocessor for Top-Down Theorem Provers. Johann Schumann.
Desiderata for Interactive Verification Systems. Konrad Slind and Christian Prehofer.
A Prolog technology theorem prover: implementation by an extended Prolog compiler. Mark Stickel.