Tom Melham
Tom Melham
Professor of Computer Science, University of Oxford
Verified email at cs.ox.ac.uk - Homepage
Title
Cited by
Cited by
Year
Introduction to HOL A theorem proving environment for higher order logic
MJC Gordon, TF Melham
25791993
Hardware verification using higher-order logic
A Camilleri, M Gordon, T Melham
University of Cambridge, Computer Laboratory, 1986
2021986
Automating recursive type definitions in higher order logic
TF Melham
Current trends in hardware verification and automated theorem proving, 341-386, 1989
1931989
Higher order logic and hardware verification
TF Melham
Cambridge University Press, 2009
1702009
Abstraction mechanisms for hardware verification
TF Melham
VLSI Specification, Verification and Synthesis, 267-291, 1988
1471988
Five axioms of alpha-conversion
AD Gordon, T Melham
International Conference on Theorem Proving in Higher Order Logics, 173-190, 1996
1201996
An industrially effective environment for formal hardware verification
CJH Seger, RB Jones, JW O'Leary, T Melham, MD Aagaard, C Barrett, ...
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions …, 2005
1172005
A Mechanized Theory of the Pi-Calculus in HOL.
TF Melham
Nord. J. Comput. 1 (1), 50-76, 1994
1121994
The PROSPER toolkit
LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ...
International Conference on Tools and Algorithms for the Construction and …, 2000
1102000
A package for inductive relation definitions in HOL
T Melham
1071992
Reasoning with inductively defined relations in the HOL theorem prover
J Camilleri, T Melham
Computer Laboratory ‚University of Cambridge, 1992
931992
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, 2006
852006
Practical formal verification in microprocessor design
RB Jones, JW O'Leary, CJH Seger, MD Aagaard, TF Melham
IEEE design & test of computers 18 (4), 16-25, 2001
592001
Dynamic specialisation of XC6200 FPGAs by partial evaluation
N McKay, S Singh
International Workshop on Field Programmable Logic and Applications, 298-307, 1998
531998
A methodology for large-scale hardware verification
MD Aagaard, RB Jones, TF Melham, JW O’leary, CJH Seger
International Conference on Formal Methods in Computer-Aided Design, 300-319, 2000
482000
Formalizing abstraction mechanisms for hardware verification in higher order logic
TF Melham
University of Cambridge, Computer Laboratory, 1990
461990
2OBJ: a metalogical framework theroem prover based on equational logic
J Goguen, A Stevens, H Hilberdink, K Hobley
Philosophical Transactions of the Royal Society of London. Series A …, 1992
451992
The HOL logic extended with quantification over type variables
TF Melham
Formal Methods in System Design 3 (1), 7-24, 1993
381993
Formal co-validation of low-level hardware/software interfaces
A Horn, M Tautschnig, C Val, L Liang, T Melham, J Grundy, D Kroening
2013 Formal Methods in Computer-Aided Design, 121-128, 2013
362013
Interactive theorem proving: An empirical study of user activity
JS Aitken, P Gray, T Melham, M Thomas
Journal of Symbolic Computation 25 (2), 263-284, 1998
351998
The system can't perform the operation now. Try again later.
Articles 1–20