| A reflective functional language for hardware design and theorem proving J Grundy, T Melham, J O'leary Journal of Functional Programming 16 (2), 157-196, 2005 | 92 | 2005 |
| The refinement calculator: Proof support for program refinement MJ Butler, J Grundy, T Långbacka, R Ruksenas, J von Wright Formal Methods Pacific, 40-61, 1997 | 88 | 1997 |
| Structured calculational proof R Back, J Grundy, J von Wright Formal Aspects of Computing 9 (5), 469-483, 1997 | 72 | 1997 |
| Structured calculational proof R Back, J Grundy, J Von Wright Tech. Rpt 65, 1996 | 72 | 1996 |
| A window inference tool for refinement J Grundy Refinement Workshop, 230-254, 1992 | 68 | 1992 |
| Ground interpolation for the theory of equality A Fuchs, A Goel, J Grundy, S Krstić, C Tinelli Tools and Algorithms for the Construction and Analysis of Systems, 413-427, 2009 | 56 | 2009 |
| Window inference in the HOL system J Grundy HOL Theorem Proving System and Its Applications, 177-189, 1991 | 54 | 1991 |
| Formal co-validation of low-level hardware/software interfaces A Horn, M Tautschnig, C Val, L Liang, T Melham, J Grundy, D Kroening Formal Methods in Computer-Aided Design (FMCAD), 2013, 121-128, 2013 | 50 | 2013 |
| Combined satisfiability modulo parametric theories S Krstić, A Goel, J Grundy, C Tinelli Tools and Algorithms for the Construction and Analysis of Systems, 602-617, 2007 | 44 | 2007 |
| Transformational hierarchical reasoning J Grundy Computer Journal 39 (4), 291-302, 1996 | 43 | 1996 |
| A method of program refinement J Grundy University of Cambridge, 1993 | 31 | 1993 |
| Methods and systems for an interactive theorem-proving tool with reflective capabilities JD Grundy, MD Aagaard US Patent 7,181,729, 2007 | 24 | 2007 |
| A browsable format for proof presentation J Grundy Mathesis Universalis 1 (2), 1996 | 23 | 1996 |
| Synthesizable high level hardware descriptions J Gillenwater, G Malecha, C Salama, AY Zhu, W Taha, J Grundy, ... New Generation Computing 28 (4), 339-369, 2010 | 21* | 2010 |
| Synthesizable High Level Hardware Descriptions: Using statically typed two-level languages to guarantee verilog synthesizability W Taha, J Gillenwater, G Malecha, C Salama, A Yun Zhu, J Grundy, ... PEPM'08: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation …, 2008 | 17* | 2008 |
| Predicative programming—A survey J Grundy Formal Methods in Programming and Their Applications, 8-25, 1993 | 14* | 1993 |
| Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs' 96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland J von Wright, J Grundy, J Harrison Springer-Verlag, 1996 | 13* | 1996 |
| Static consistency checking for Verilog wire interconnects: Using dependent types to check the sanity of Verilog descriptions C Salama, G Malecha, W Taha, J Grundy, J O'Leary Partial evaluation and program manipulation, 121-130, 2009 | 12 | 2009 |
| Tool building requirements for an API to first-order solvers J Grundy, T Melham, S Krstić, S McLaughlin Electronic Notes in Theoretical Computer Science 144 (2), 15-26, 2006 | 8 | 2006 |
| International Refinement Workshop and Formal Methods Pacific: Proceedings of IRW/FMP'98 J Grundy, M Schwenke, T Vickers Springer, 1998 | 8* | 1998 |
John O'LearyIntel CorporationVerified email at intel.com
