2009 |
34 | EE | Magnus O. Myreen,
Konrad Slind,
Michael J. C. Gordon:
Extensible Proof-Producing Compilation.
CC 2009: 2-16 |
2008 |
33 | EE | Guodong Li,
Konrad Slind:
Trusted Source Translation of a Total Function Language.
TACAS 2008: 471-485 |
32 | EE | Konrad Slind,
Michael Norrish:
A Brief Overview of HOL4.
TPHOLs 2008: 28-32 |
2007 |
31 | EE | Guodong Li,
Konrad Slind:
Compilation as Rewriting in Higher Order Logic.
CADE 2007: 19-34 |
30 | EE | Guodong Li,
Scott Owens,
Konrad Slind:
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic.
ESOP 2007: 205-219 |
29 | EE | Matt Kaufmann,
Konrad Slind:
Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0.
TPHOLs 2007: 294-301 |
28 | EE | Konrad Slind,
Scott Owens,
Juliano Iyoda,
Mike Gordon:
Proof producing synthesis of arithmetic and cryptographic hardware.
Formal Asp. Comput. 19(3): 343-362 (2007) |
2006 |
27 | EE | John Harrison,
Konrad Slind,
Rob Arthan:
HOL.
The Seventeen Provers of the World 2006: 11-19 |
26 | EE | 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) |
2005 |
25 | EE | Sudhindra Pandav,
Konrad Slind,
Ganesh Gopalakrishnan:
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.
CHARME 2005: 317-331 |
24 | EE | Jianjun Duan,
Joe Hurd,
Guodong Li,
Scott Owens,
Konrad Slind,
Junxing Zhang:
Functional Correctness Proofs of Encryption Algorithms.
LPAR 2005: 519-533 |
23 | EE | Michael Norrish,
Konrad Slind:
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.
TPHOLs 2005: 397-408 |
22 | EE | Annette Bunker,
Ganesh Gopalakrishnan,
Konrad Slind:
Live sequence charts applied to hardware requirements specification and verification.
STTT 7(4): 341-350 (2005) |
2004 |
21 | | Konrad Slind,
Annette Bunker,
Ganesh Gopalakrishnan:
Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings
Springer 2004 |
20 | EE | Yue Yang,
Ganesh Gopalakrishnan,
Gary Lindstrom,
Konrad Slind:
Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models.
IPDPS 2004 |
2003 |
19 | EE | 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 |
18 | EE | Yue Yang,
Ganesh Gopalakrishnan,
Gary Lindstrom,
Konrad Slind:
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT.
CHARME 2003: 81-95 |
17 | EE | Konrad Slind,
Joe Hurd:
Applications of Polytypism in Theorem Proving.
TPHOLs 2003: 103-119 |
16 | EE | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Thomas F. Melham:
The PROSPER toolkit.
STTT 4(2): 189-210 (2003) |
2002 |
15 | EE | Michael Norrish,
Konrad Slind:
A Thread of HOL Development.
Comput. J. 45(1): 37-45 (2002) |
2000 |
14 | | Konrad Slind:
Wellfounded Schematic Definitions.
CADE 2000: 45-63 |
13 | EE | Richard J. Boulton,
Konrad Slind:
Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions.
Computational Logic 2000: 629-643 |
12 | EE | 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 |
11 | | Konrad Slind:
Another Look at Nested Recursion.
TPHOLs 2000: 498-518 |
1998 |
10 | EE | Konrad Slind,
Michael J. C. Gordon,
Richard J. Boulton,
Alan Bundy:
System Description: An Interface Between CLAM and HOL.
CADE 1998: 134-138 |
9 | | Richard J. Boulton,
Konrad Slind,
Alan Bundy,
Michael J. C. Gordon:
An Interface between Clam and HOL.
TPHOLs 1998: 87-104 |
1997 |
8 | | Konrad Slind:
Derivation and Use of Induction Schemes in Higher-Order Logic.
TPHOLs 1997: 275-290 |
7 | | Olaf Müller,
Konrad Slind:
Treating Partiality in a Logic of Total Functions.
Comput. J. 40(10): 640-652 (1997) |
1996 |
6 | | Konrad Slind:
Function Definition in Higher-Order Logic.
TPHOLs 1996: 381-397 |
1994 |
5 | | Konrad Slind:
A Parameterized Proof Manager.
TPHOLs 1994: 407-423 |
4 | | Tobias Nipkow,
Konrad Slind:
I/Q Automata in Isabelle/HOL.
TYPES 1994: 101-119 |
1993 |
3 | | Konrad Slind:
AC Unification in HOL90.
HUG 1993: 436-449 |
1992 |
2 | | Konrad Slind:
Adding New Rules to an LCF-style Logic Implementation.
TPHOLs 1992: 549-559 |
1987 |
1 | EE | Jeffrey Joyce,
Greg Lomow,
Konrad Slind,
Brian Unger:
Monitoring Distributed Systems.
ACM Trans. Comput. Syst. 5(2): 121-150 (1987) |