Papers

• Konrad Slind and Michael Norrish, An Implementation of Higher Order Logic, February 2001.
  DRAFT

• Konrad Slind, Modelling and Reasoning about Functional Programs in Higher Order Logic, December 2000.
  Slides for a talk given at the University of Calgary and the University of Victoria.

• Michael Norrish and Konrad Slind, A Thread of HOL Development, June 2000.
  To appear in The Computer Journal in a special issue in honour of Graham Birtwistle.
  DRAFT (revised, but comments still welcome).

• Konrad Slind, PROSPER Database,May 2000.

• Konrad Slind, PROSPER Theory Management Subsystem:Discussion and Proposal, March 2000.

• Konrad Slind, Another Look at Nested Recursion. Appears in Proceedings of TPHOLs2000 (LNCS 1869).

• Mike Gordon, David Greaves, and Konrad Slind, Extracting Behaviour from Synthesized Verilog. Appears in Supplementary Proceedings of TPHOLs2000.

• Richard Boulton and Konrad Slind, Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions. Appears in Proceedings of CL2000 (LNAI 1861).

• Konrad Slind, Wellfounded Schematic Definitions. Appears in Proceedings of CADE-17 (LNCS 1831).

• Konrad Slind, Reasoning about Terminating Functional Programs
  PhD Thesis TU Munich. Oral Exam November 15, 1999.

• Louise Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, Mike Gordon, and Tom Melham, The PROSPER Toolkit. Appears in Proceedings of TACAS'2000 (LNCS 1785).
  (Awarded a best paper prize sponsored by the STTT journal.)

• Konrad Slind and Richard Boulton, Iterative Dialogues and Automated Proof. Presented at FroCoS'98. Published in Frontiers of Combining Systems 2, Editors D. Gabbay and M. de Rijke, Number 7 in Studies in Logic and Computation, Research Studies Press, 2000.

• Konrad Slind, A Tagged LCF-style Proof Architecture, Presented at LD98.

• Richard Boulton, Konrad Slind, Alan Bundy, and Mike Gordon, An Interface between Clam and HOL. Appears in Proceedings of TPHOLs98 (LNCS 1479).

• Olaf Mueller and Konrad Slind, Treating Partiality in a Logic of Total Functions. Appears in The Computer Journal 40(10), 1997.

• Konrad Slind, Derivation and Use of Induction Schemes in Higher-Order Logic. Appears in Proceedings of TPHOLs97 (LNCS 1275).

• Konrad Slind, Function Definition in Higher Order Logic. Appears in Proceedings of TPHOLs 96 (LNCS 1125).

• Tobias Nipkow and Konrad Slind, I/O Automata in Isabelle/HOL, Appears in Proceedings of the June 1994 TYPES workshop in Båstad, Sweden (LNCS 996).

• Konrad Slind and Christian Prehofer, Desiderata for Interactive Verification Systems, DFG project report, 29 pages, February 1994.

• Konrad Slind, A Parameterized Proof Manager, Appears in Proceedings of the 1994 HOL Users Group Meeting, Malta (LNCS 859).

• John Harrison and Konrad Slind, A Reference Implementation of HOL, Draft paper, presented at the poster session of the 1994 HOL Users Group Meeting, Malta.

• Konrad Slind, AC Unification in hol90, Appeared in Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications August 1993, Vancouver, Editors J. Joyce and C.-J. Seger, (LNCS 780)

• Konrad Slind, Adding new rules to an LCF-style logic implementation: Preliminary report, Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications, Sept. 1992, Leuven, Belgium, Editors L. Claesen and M. Gordon, Elsevier Science Publishers.

• Konrad Slind, Object Language Embedding in Standard ML of New Jersey, Proceedings of the Second ML Workshop held at Carnegie Mellon University, Pittsbugh, Pennsylvania, September 26-27, 1991, CMU SCS Technical Report, November 1991 Note. The paper is up-to-date with respect to the quote/antiquote facility, but not with respect to prettyprinting, which has been generalized in subsequent releases of SML/NJ (version 0.93 and later).

• Konrad Slind. An implementation of higher order logic. Master's Thesis, January 1991, Research Report No. 91/419/03, Department of Computer Science, University of Calgary.

• Konrad Slind, Completion as a Derived Rule of Inference, Research Report 90/409/33, Department of Computer Science, University of Calgary, Calgary, Alberta, October 1990.

• Graham Birtwistle, Brian Graham, Todd Simpson, Konrad Slind, Mark Williams, and Simon Williams, Verifying an SECD Chip in HOL, Proceeding of the IFIP WG 10.2/WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design, North Holland, 1990, pp. 369-378 .

• Konrad Slind, Graham Birtwistle, Mike Hermann, and Todd Simpson, From Logic to Layout: transforming HOL specifications into gate array netlists, Canadian Conference on Electrical and Computer Engineering, Montreal, 1989, pp. 352-355.

• Graham Birtwistle, Mike Hermann, Todd Simpson, and Konrad Slind, From formal proof to netlist, Canadian Conference on VLSI, Vancouver 1989, pp. 217-224.

• Jeffrey Joyce, Greg Lomow, Konrad Slind, and Brian Unger, Monitoring Distributed Systems, ACM Transactions on Computer Systems, Vol. 5 , No. 2, May 1987, pp. 121-150.

• Brian Unger, John Cleary, Greg Lomow, Li Xining, Xiao Zhonge, and Konrad Slind, Jade Virtual Time Implementation Manual, Research Report 86/242/16, Department of Computer Science, University of Calgary, Calgary, Alberta, 1986.