Konrad Slind

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)

Coauthor Index

1	Rob Arthan	[27]
2	Richard J. Boulton	[9] [10] [12] [13] [16]
3	Alan Bundy	[9] [10]
4	Annette Bunker	[21] [22]
5	Graham Collins	[12] [16]
6	Louise A. Dennis	[12] [16]
7	Jianjun Duan	[24]
8	Ganesh Gopalakrishnan	[18] [20] [21] [22] [25]
9	Michael J. C. Gordon	[9] [10] [12] [19] [34]
10	Mike Gordon	[26] [28]
11	John Harrison	[27]
12	Joe Hurd	[17] [19] [24]
13	Juliano Iyoda	[26] [28]
14	Jeffrey Joyce	[1]
15	Matt Kaufmann	[29]
16	Guodong Li	[24] [30] [31] [33]
17	Gary Lindstrom	[18] [20]
18	Greg Lomow	[1]
19	Thomas F. Melham	[12] [16]
20	Olaf Müller	[7]
21	Magnus O. Myreen	[34]
22	Tobias Nipkow	[4]
23	Michael Norrish	[12] [15] [16] [23] [32]
24	Scott Owens	[24] [26] [28] [30]
25	Sudhindra Pandav	[25]
26	Graham Robinson	[12]
27	Brian Unger	[1]
28	Yue Yang	[18] [20]
29	Junxing Zhang	[24]

Colors in the list of coauthors