Publications

• Magnus Myreen, Konrad Slind and Mike Gordon
  Machine-code verification for multiple architectures: an application of decompilation into logic,
  submitted to FMCAD 2008.

• Konrad Slind and Michael Norrish
  A Brief Overview of HOL4,
  TPHOLs 2008.

• Guodong Li and Konrad Slind
  Trusted Source Tranlstion of a Total Function Language,
  TACAS 2008.

• Matt Kaufmann and Konrad Slind
  Wellfounded Induction on the Ordinals up to Epsilon-0,
  TPHOLs 2007.

• Guodong Li and Konrad Slind,
  Compilation as Rewriting in Higher Order Logic,
  CADE 2007

• Scott Owens and Konrad Slind,
  Adapting Functional Programs to Higher Order Logic,
  to appear in Higher Order and Symbolic Computation.

• Konrad Slind, Scott Owens, Juliano Iyoda, and Mike Gordon,
  Proof producing synthesis of arithmetic and cryptographic hardware,
  to appear in Formal Aspects of Computing.

• Guodong Li, Scott Owens, and Konrad Slind,
  Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic,
  ESOP 2007

• John Harrison, Konrad Slind, Rob Arthan, "HOL",
  appears in The Seventeen Provers of the World LNCS 3600

• Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, and Junxing Zhang.
  Functional Correctness Proofs of Encryption Algorithms,
  LPAR 2005.

• Sudhindra Pandav, Konrad Slind, and Ganesh Gopalakrishnan.
  Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification,
  CHARME 2005.

• Michael Norrish and Konrad Slind.
  Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof,
  TPHOLs 2005.

• Junxing Zhang and Konrad Slind.
  Verification of Euclid's Algorithm for Finding Multiplicative Inverses ,
  TPHOLs 2005, Emerging Trends.

• Mike Gordon, Juliano Iyoda, Scott Owens, and Konrad Slind.
  A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic,
  TPHOLs 2005, Emerging Trends.

• Konrad Slind,Steven Barrus, Seungkeol Choe, Chris Condrat, Jianjun Duan, Sivaram Gopalakrishnan, Aaron Knoll, Hiro Kuwahara, Guodong Li, Scott Little, Lei Liu, Steffanie Moore, Robert Palmer, Claurissa Tuttle, Sean Walton, Yu Yang, and Junxing Zhang.
  Teaching a HOL Course: Experience Report,
  TPHOLs 2005, Emerging Trends.

• Mike Gordon, Juliano Iyoda, Scott Owens, and Konrad Slind.
  Automatic Formal Synthesis of Hardware from Higher Order Logic,
  AVoCS 2005.

• Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan.
  Theorem Proving in Higher Order Logics (TPHOLs 2004) Park City, Utah. LNCS 3223

• Scott Owens and Konrad Slind, Proving as Programming with DrHOL: A Preliminary Design,
  Proceedings of UITP 2003

• Jason Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slind.
  Analyzing the Intel Itanium Memory Ordering using Logic Programming and SAT,
  Proceedings of CHARME 2003

• Mike Gordon, Joe Hurd, and Konrad Slind.
  Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving,
  Proceedings of CHARME 2003

• Konrad Slind and Joe Hurd.
  Applications of Polytypism in Theorem Proving,
  At TPHOLs'03, Rome Italy.
  Preliminary slides in PDF

• Konrad Slind.
  A Verification of Rijndael in HOL, August 2002. Transparencies.
  Appears in Supplementary Proceedings of TPHOLs'02, NASA Conference Proceedings CP-2002-211736.

• Konrad Slind and Michael Norrish, The K combinator as a semantically transparent tagging mechanism, August 2002.
  Appears in Supplementary Proceedings of TPHOLs'02, NASA Conference Proceedings CP-2002-211736.

• Konrad Slind and Michael Norrish, An Implementation of Higher Order Logic, February 2001.
  DRAFT, to appear in forthcoming Prosper book

• Michael Norrish and Konrad Slind, A Thread of HOL Development, in The Computer Journal Volume 45(1), 2002. Special issue in honour of Graham Birtwistle.

• 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.

• 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.