Tom Melham
Tom Melham
Professor of Computer Science, University of Oxford
Verified email at - Homepage
Cited by
Cited by
Introduction to HOL: a theorem proving environment for higher order logic
MJC Gordon, TF Melham
Cambridge University Press, 1993
Hardware verification using higher-order logic
A Camilleri, M Gordon, T Melham
University of Cambridge, Computer Laboratory, 1986
Automating recursive type definitions in higher order logic
TF Melham
Current trends in hardware verification and automated theorem proving, 341-386, 1989
Higher order logic and hardware verification
TF Melham
Cambridge University Press, 2009
Abstraction mechanisms for hardware verification
TF Melham
VLSI Specification, Verification and Synthesis, 267-291, 1988
Five axioms of alpha-conversion
AD Gordon, T Melham
International Conference on Theorem Proving in Higher Order Logics, 173-190, 1996
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
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
A Mechanized Theory of the Pi-Calculus in HOL.
TF Melham
Nord. J. Comput. 1 (1), 50-76, 1994
A package for inductive relation definitions in HOL
T Melham
Reasoning with inductively defined relations in the HOL theorem prover
J Camilleri, T Melham
Computer Laboratory ‚University of Cambridge, 1992
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
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
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
Dynamic specialisation of XC6200 FPGAs by partial evaluation
N McKay, S Singh
International Workshop on Field Programmable Logic and Applications, 298-307, 1998
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
Formalizing abstraction mechanisms for hardware verification in higher order logic
TF Melham
University of Cambridge, Computer Laboratory, 1990
The HOL logic extended with quantification over type variables
TF Melham
Formal Methods in System Design 3 (1-2), 7-24, 1993
Using recursive types to reason about hardware in higher order logic
TF Melham
International Working Conference on The Fusion of Hardware Design and …, 1988
Translating dependent type theory into higher order logic
B Jacobs, T Melham
International Conference on Typed Lambda Calculi and Applications, 209-229, 1993
The system can't perform the operation now. Try again later.
Articles 1–20