Tom Melham
Tom Melham
Professor of Computer Science, University of Oxford
Verified email at cs.ox.ac.uk - Homepage
TitleCited byYear
Introduction to HOL A theorem proving environment for higher order logic
MJC Gordon, TF Melham
24901993
Hardware verification using higher-order logic
A Camilleri, M Gordon, T Melham
University of Cambridge, Computer Laboratory, 1986
2031986
Automating recursive type definitions in higher order logic
TF Melham
Current trends in hardware verification and automated theorem proving, 341-386, 1989
1861989
Higher order logic and hardware verification
TF Melham
Cambridge University Press, 2009
1642009
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
1171996
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
1112005
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
1082000
A Mechanized Theory of the Pi-Calculus in HOL.
TF Melham
Nord. J. Comput. 1 (1), 50-76, 1994
1041994
A package for inductive relation definitions in HOL
T Melham
981992
Reasoning with inductively defined relations in the HOL theorem prover
J Camilleri, T Melham
Computer Laboratory ‚University of Cambridge, 1992
921992
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
832006
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
602001
Dynamic specialisation of XC6200 FPGAs by partial evaluation
N McKay, S Singh
International Workshop on Field Programmable Logic and Applications, 298-307, 1998
491998
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
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
481992
Formalizing abstraction mechanisms for hardware verification in higher order logic
TF Melham
University of Cambridge, Computer Laboratory, 1990
451990
The HOL logic extended with quantification over type variables
TF Melham
Formal Methods in System Design 3 (1-2), 7-24, 1993
401993
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
331998
Translating dependent type theory into higher order logic
B Jacobs, T Melham
International Conference on Typed Lambda Calculi and Applications, 209-229, 1993
331993
The system can't perform the operation now. Try again later.
Articles 1–20