Konrad Slind

David Greve, Konrad Slind: A Step-Indexing Approach to Partial Functions. ACL2 2013: 42-53

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind: Decompilation into logic - Improved. FMCAD 2012: 78-81

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham: A DSL for cross-domain security. HILT 2012: 53-62

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham: The Guardol Language and Verification System. TACAS 2012: 18-32

Richard J. Boulton, Joe Hurd, Konrad Slind: Computer Assisted Reasoning. J. Autom. Reasoning 43(3): 237-242 (2009)

Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon: Extensible Proof-Producing Compilation. CC 2009: 2-16

Scott Owens, Konrad Slind: Adapting functional programs to higher order logic. Higher-Order and Symbolic Computation 21(4): 377-409 (2008)

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind: Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD 2008: 1-8

Guodong Li, Konrad Slind: Trusted Source Translation of a Total Function Language. TACAS 2008: 471-485

Konrad Slind, Michael Norrish: A Brief Overview of HOL4. TPHOLs 2008: 28-32

Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon: Proof producing synthesis of arithmetic and cryptographic hardware. Formal Asp. Comput. 19(3): 343-362 (2007)

Guodong Li, Konrad Slind: Compilation as Rewriting in Higher Order Logic. CADE 2007: 19-34

Guodong Li, Scott Owens, Konrad Slind: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. ESOP 2007: 205-219

Matt Kaufmann, Konrad Slind: Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon ₀. TPHOLs 2007: 294-301

Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind: Automatic Formal Synthesis of Hardware from Higher Order Logic. Electr. Notes Theor. Comput. Sci. 145: 27-43 (2006)

John Harrison, Konrad Slind, Rob Arthan: HOL. The Seventeen Provers of the World 2006: 11-19

Annette Bunker, Ganesh Gopalakrishnan, Konrad Slind: Live sequence charts applied to hardware requirements specification and verification. STTT 7(4): 341-350 (2005)

Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan: Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. CHARME 2005: 317-331

Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang: Functional Correctness Proofs of Encryption Algorithms. LPAR 2005: 519-533

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

Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind: Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models. IPDPS 2004

Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (Eds.): Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings. Lecture Notes in Computer Science 3223, Springer 2004, isbn 3-540-23017-3

Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham: The PROSPER toolkit. STTT 4(2): 189-210 (2003)

Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind: Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. CHARME 2003: 81-95

Michael J. C. Gordon, Joe Hurd, Konrad Slind: Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. CHARME 2003: 200-215

Konrad Slind, Joe Hurd: Applications of Polytypism in Theorem Proving. TPHOLs 2003: 103-119

Michael Norrish, Konrad Slind: A Thread of HOL Development. Comput. J. 45(1): 37-45 (2002)

Konrad Slind: Wellfounded Schematic Definitions. CADE 2000: 45-63

Richard J. Boulton, Konrad Slind: Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions. Computational Logic 2000: 629-643

Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham: The PROSPER Toolkit. TACAS 2000: 78-92

Konrad Slind: Another Look at Nested Recursion. TPHOLs 2000: 498-518

Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy: System Description: An Interface Between CL^AM and HOL. CADE 1998: 134-138

Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon: An Interface between Clam and HOL. TPHOLs 1998: 87-104

Olaf Müller, Konrad Slind: Treating Partiality in a Logic of Total Functions. Comput. J. 40(10): 640-652 (1997)

Konrad Slind: Derivation and Use of Induction Schemes in Higher-Order Logic. TPHOLs 1997: 275-290

Konrad Slind: Function Definition in Higher-Order Logic. TPHOLs 1996: 381-397

Konrad Slind: A Parameterized Proof Manager. TPHOLs 1994: 407-423

Tobias Nipkow, Konrad Slind: I/Q Automata in Isabelle/HOL. TYPES 1994: 101-119

Konrad Slind: AC Unification in HOL90. HUG 1993: 436-449

Konrad Slind: Adding New Rules to an LCF-style Logic Implementation. TPHOLs 1992: 549-559

Jeffrey Joyce, Greg Lomow, Konrad Slind, Brian Unger: Monitoring Distributed Systems. ACM Trans. Comput. Syst. 5(2): 121-150 (1987)