| [1] | T. Melham. Higher Order Logic and Hardware Verification, volume 31 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993. [ bib | .html ] |
| [2] | Joe Hurd and Tom Melham, editors. Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005: Oxford, UK, August 22-25, 2005: Proceedings, volume 3603 of Lecture Notes in Computer Science. Springer-Verlag, 2005. [ bib | http ] |
| [3] | Tiziana Margaria and Tom Melham, editors. Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001: Livingston, Scotland, UK, September 4-7 2001: Proceedings, volume 2144 of Lecture Notes in Computer Science. Springer-Verlag, 2001. [ bib | http ] |
| [4] | Thomas F. Melham and Juanito Camilleri, editors. Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: Valletta, Malta, September 19-22, 1994: Proceedings, volume 859 of Lecture Notes in Computer Science. Springer-Verlag, 1994. [ bib ] |
| [5] | M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. [ bib | .html ] |
| [6] | V. Stavridou, T. F. Melham, and R. T. Boute, editors. Theorem Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience: Nijmegen, The Netherlands, 22-24 June 1992, volume 10 of IFIP Transactions A. North-Holland, 1992. [ bib ] |
| [7] | Thomas Frederick Melham. Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic. PhD thesis, University of Cambridge, August 1989. [ bib ] |
| [8] |
Zurab Khasidashvili, Gavriel Gavrielov, and Tom Melham.
Assume-guarantee validation for STE properties within an SVA
environment.
In Armin Biere and Carl Pixley, editors, Proceedings of 9th
International Conference: 2009 Formal Methods in Computer-Aided Design:
FMCAD 2009, pages 108-115. IEEE, 2009. [ bib | .pdf ] |
| [9] |
Peter Böhm and Tom Melham.
A refinement approach to design and verification of on-chip
communication protocols.
In Alessandro Cimatti and Robert B. Jones, editors, 2008 Formal
Methods in Computer Aided Design: Portland, Oregon, USA: 17-20
November 2008, pages 136-143. IEEE, 2008. [ bib | .pdf ] |
| [10] |
Sara Adams, Magnus Björk, Tom Melham, and Carl-Johan Seger.
Automatic abstraction in symbolic trajectory evaluation.
In Jason Baumgartner and Mary Sheeran, editors, Formal Methods
in Computer Aided Design: FMCAD 2007: November 11-14 2007, Austin,
Texas, USA, pages 127-135. IEEE Computer Society, 2007. [ bib | .pdf ] |
| [11] |
Ziyad Hanna and Tom Melham.
Early validation of computer microarchitecture with algorithm level
models.
In Andreas Prinz, editor, Proceedings of ASM'07: The 14th
International Abstract State Machines Workshop, 2007.
Published electronically. [ bib | .pdf ] |
| [12] |
Jim Grundy, Tom Melham, and John O'Leary.
A reflective functional language for hardware design and theorem
proving.
Journal of Functional Programming, 16(2):157-196, March 2006. [ bib | .pdf ] |
| [13] |
Jim Grundy, Tom Melham, Sava Krstic, and Sean McLaughlin.
Tool building requirements for an api to first-order solvers.
Electronic Notes in Theoretical Computer Science,
144(2):15-26, January 2006. [ bib | .pdf ] |
| [14] |
Carl-Johan H. Seger, Robert B. Jones, John W. O'Leary, Tom Melham, Mark D.
Aagaard, Clark Barrett, and Don Syme.
An industrially effective environment for formal hardware
verification.
IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, 24(9):1381-1405, September 2005. [ bib | .pdf ] |
| [15] |
Kong Woei Susanto and Tom Melham.
An AMBA-ARM7 formal verification platform.
In Jin Song Dong and Jim Woodcock, editors, Formal Methods and
Software Engineering: 5th International Conference on Formal Engineering
Methods, ICFEM 2003: Singapore, November 5-7, 2003: Proceedings,
volume 2885 of Lecture Notes in Computer Science, pages 48-67.
Springer-Verlag, 2003. [ bib | .pdf ] |
| [16] |
Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad
Slind, and Thomas F. Melham.
The PROSPER toolkit.
International Journal on Software Tools for Technology
Transfer, 4(2):189-210, February 2003. [ bib | http ] |
| [17] |
Thomas F. Melham and Robert B. Jones.
Abstraction by symbolic indexing transformations.
In Mark D. Aagaard and John W. O'Leary, editors, Formal Methods
in Computer-Aided Design: 4th International Conference, FMCAD 2002:
Portland, OR, USA, November 6-8, 2002: Proceedings, volume 2517
of Lecture Notes in Computer Science, pages 1-18. Springer-Verlag,
2002. [ bib | .pdf ] |
| [18] |
Robert B. Jones, John W. O'Leary, Carl-Johan H. Seger, Mark D. Aagaard, and
Thomas F. Melham.
Practical formal verification in microprocessor design.
IEEE Design & Test of Computers, 18(4):16-25, July/August
2001. [ bib | .pdf ] |
| [19] |
Kong Woei Susanto and Tom Melham.
Formally analyzed dynamic synthesis of hardware.
The Journal of Supercomputing, 19(1):7-22, May 2001. [ bib | .ps ] |
| [20] |
Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, and
Carl-Johan H. Seger.
A methodology for large-scale hardware verification.
In Warren A. Hunt, Jr. and Steven D. Johnson, editors, Formal
Methods in Computer-Aided Design: Third International Conference, FMCAD
2000: Austin, TX, USA, November 1-3, 2000: Proceedings, volume
1954 of Lecture Notes in Computer Science, pages 263-282.
Springer-Verlag, 2000. [ bib | .pdf ] |
| [21] |
S. Aitken and T. Melham.
An analysis of errors in interactive proof attempts.
Interacting with Computers, 12(6):565-586, June 2000. [ bib ] |
| [22] |
Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad
Slind, Graham Robinson, Mike Gordon, and Tom Melham.
The PROSPER toolkit.
In Susanne Graf and Michael Schwartzbach, editors, Tools and
Algorithms for the Construction and Analysis of Systems: 6th International
Conference, TACAS 2000: Held as Part of the Joint European Conferences on
Theory and Practice of Software, ETAPS 2000: Berlin, Germany, March
25 - April 2, 2000: Proceedings, volume 1785 of Lecture Notes in
Computer Science, pages 78-92. Springer-Verlag, 2000. [ bib | .pdf ] |
| [23] |
Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary.
Xs are for trajectory evaluation, Booleans are for theorem
proving.
In Laurence Pierre and Thomas Kropf, editors, Correct Hardware
Design and Verification Methods: 10th IFIP WG10.5 Advanced Research
Working Conference, CHARME'99: Bad Herrenalb, Germany, September
27-29, 1999: Proceedings, volume 1703 of Lecture Notes in Computer
Science, pages 202-218. Springer-Verlag, 1999. [ bib | .pdf ] |
| [24] |
Nicholas McKay, Tom Melham, Kong Woei Susanto, and Satnam Singh.
Dynamic specialisation of XC6200 FPGAs by partial evaluation.
In Kenneth L. Pocek and Jeffrey M. Arnold, editors, Proceedings:
IEEE Symposium on FPGAs for Custom Computing Machines: April 15-17,
1998, Napa Valley, California, pages 308-309. IEEE Computer Society,
1998. [ bib | .pdf ] |
| [25] |
J. S. Aitken, P. Gray, T. Melham, and M. Thomas.
Interactive theorem proving: An empirical study of user activity.
Journal of Symbolic Computation, 25(2):263-284, February 1998. [ bib ] |
| [26] |
Andrew D. Gordon and Tom Melham.
Five axioms of alpha-conversion.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, TPHOLs'96:
Turku, Finland, August 26-30, 1996: Proceedings, volume 1125 of
Lecture Notes in Computer Science, pages 173-190. Springer-Verlag, 1996. [ bib | .pdf ] |
| [27] |
J. S. Aitken, P. Gray, T. Melham, and M. Thomas.
Phases, modes and information flow in theory development.
In Nicholas A. Merriam, editor, User Interfaces for Theorem
Provers: An International Workshop organised at the Department of
Computer Science, University of York: 19th July 1996, pages 1-8.
University of York, 1996. [ bib ] |
| [28] |
T. F. Melham.
A mechanized theory of the Pi-calculus in HOL.
Nordic Journal of Computing, 1(1):50-76, 1994. [ bib ] |
| [29] |
Thomas F. Melham.
The HOL logic extended with quantification over type variables.
Formal Methods in System Design, 3(1-2):7-24, 1994. [ bib | .pdf ] |
| [30] |
Thomas F. Melham.
The HOL logic extended with quantification over type variables.
In Luc J. M. Claesen and Michael J. C. Gordon, editors, Higher
Order Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving
and its Applications - HOL '92: Leuven, Belgium, 21-24 September
1992, volume 20 of IFIP Transactions A, pages 3-17. North-Holland,
1993. [ bib ] |
| [31] |
Bart Jacobs and Tom Melham.
Translating dependent type theory into higher order logic.
In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and
Applications: International Conference on Typed Lamda Calculi and
Applications: TLCA '93: March, 16-18, 1993, Utrecht, The
Netherlands: Proceedings, volume 664 of Lecture Notes in Computer
Science, pages 209-229. Springer-Verlag, 1993. [ bib ] |
| [32] |
T. F. Melham.
A package for inductive relation definitions in HOL.
In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J.
Windley, editors, Proceedings of the 1991 International Workshop on the
HOL Theorem Proving System and its Applications, Davis, California,
August 28-30, 1991, pages 350-357. IEEE Computer Society Press, 1992. [ bib | .pdf ] |
| [33] |
Thomas F. Melham.
Using recursive types to reason about hardware in higher order logic.
In George J. Milne, editor, The Fusion of Hardware Design and
Verification: Proceedings of the IFIP WG 10.2 Working Conference on The
Fusion of Hardware Design and Verification: Glasgow, Scotland, 4-6
July, 1988, pages 27-50. North-Holland, 1988. [ bib ] |
| [34] |
G. Birtwistle, B. Graham, T. Melham, and R. Schediwy.
Hardware verification by formal proof.
In V. K. Bhargava, editor, Proceedings of the Canadian
Conference on Electrical and Computer Engineering, Vancouver, November
1988, pages 379-384. Canadian Society for Electrical Engineering, 1988. [ bib ] |
| [35] |
Albert Camilleri, Mike Gordon, and Tom Melham.
Hardware verification using higher-order logic.
In Dominique Borrione, editor, From HDL Descriptions to
Guaranteed Correct Circuit Designs: Proceedings of the IFIP WG 10.2
Working Conference on From HDL Descriptions to Guaranteed Correct Circuit
Designs, Grenoble, France, 9-11 September, 1986, pages 43-67.
North-Holland, 1987. [ bib ] |
| [36] |
Graham Birtwistle, Jeff Joyce, Breen Liblong, Tom Melham, and Rick Schediwy.
Specification and VLSI design.
In George J. Milne and P. A. Subrahmanyam, editors, Formal
Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on
VLSI: Edinburgh, Scotland, U.K., pages 83-97. North-Holland, 1986. [ bib ] |
| [37] |
Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall.
Towards a VLSI design tool system.
INFOR: Information Systems and Operational Research,
23(4):389-402, November 1985. [ bib ] |
| [38] |
Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall.
Towards a VLSI design tool system.
In Leo Gotlieb, editor, Canadian Information Processing
Society: SESSION 84: Proceedings, pages 37-42. Canadian Information
Processing Society, 1984. [ bib ] |
| [39] |
B. Liblong, T. Melham, and G. Birtwistle.
Exploiting hierarchies in EDICT.
In Proceedings of the 1984 Canadian Conference on VLSI,
1984. [ bib ] |
| [40] |
Ziyad Hanna and Tom Melham.
A symbolic execution framework for algorithm-level modelling.
In Priyank Kalla and Prabhat Mishra, editors, High Level Design
Validation and Test Workshop, 2009. HLDVT 2009., pages 94-99. IEEE, 2009. [ bib | .pdf ] |
| [41] |
Tom Melham.
Integrating model checking and theorem proving in a reflective
functional language.
In Eerke A. Boiten, John Derrick, and Graeme Smith, editors,
Integrated Formal Methods: 4th International Conference, IFM 2004:
Canterbury, UK, April 4-7, 2004: Proceedings, volume 2999 of
Lecture Notes in Computer Science, pages 36-39. Springer-Verlag, 2004. [ bib | .pdf ] |
| [42] |
Tom Melham.
Abstract: Experience with practical formal verification at an
industrial scale.
In Clare Dixon, editor, Proceedings of the Tenth Workshop on
Automated Reasoning: Bridging the Gap between Theory and Practice: 15th-16th
April 2003: Liverpool, pages 1-2. Department of Computer Science,
University of Liverpool, 2003. [ bib | .pdf ] |
| [43] |
Thomas F. Melham.
PROSPER: An investigation into software architecture for embedded
proof engines.
In Alessandro Armando, editor, Frontiers of Combining Systems:
4th International Workshop, FroCoS 2002: Santa Margherita Ligure,
Italy, April 8-10, 2002: Proceedings, volume 2309 of Lecture Notes
in Artificial Intelligence, pages 193-206. Springer-Verlag, 2002. [ bib | .pdf ] |
| [44] |
Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas.
Interactive proof discovery: An empirical study of HOL users.
In Philip Gray, editor, User Interface Design for Theorem
Proving Systems: An International Workshop organised by the ITP Project.
Department of Computing Science, University of Glasgow, 1995. [ bib | .pdf ] |
| [45] |
T. F. Melham.
A mechanized theory of the pi-calculus in HOL.
In G. Huet and G. Plotkin, editors, Proceedings of the Second
Workshop on Logical Frameworks, pages 219-237. University of Edinburgh,
1991.
Preliminary proceedings, published electronically after the workshop. [ bib ] |
| [46] |
Thomas F. Melham.
Abstraction mechanisms for hardware verification.
In Michael Yoeli, editor, Formal Verification of Hardware
Design, pages 30-49. IEEE Computer Society Press, 1990. [ bib ] |
| [47] |
Thomas F. Melham.
Automating recursive type definitions in higher order logic.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 341-386.
Springer-Verlag, 1989. [ bib | .pdf ] |
| [48] |
Thomas F. Melham.
Abstraction mechanisms for hardware verification.
In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI
Specification, Verification and Synthesis, volume SECS35 of The Kluwer
International Series in Engineeering and Computer Science, pages 267-291.
Kluwer Academic Publishers, 1988. [ bib ] |
| [49] |
Peter Böhm and Tom Melham.
Design and verification of on-chip communication protocols.
Research Report RR-08-05, Oxford University Computing Laboratory,
April 2008. [ bib | .pdf ] |
| [50] |
Peter Böhm and Tom Melham.
Design and verification of on-chip communication protocols.
In Gordon J. Pace and Satnam Singh, editors, Seventh
International Workshop on Designing Correct Circuits: Budapest,
29-30 March 2008: Participants' Proceedings, pages 15-29. ETAPS 2008,
March 2008.
A Satellite Event of the ETAPS 2008 group of conferences. [ bib | .pdf ] |
| [51] |
Tom Melham and John O'Leary.
A functional HDL in reFLect.
In Mary Sheeran and Tom Melham, editors, Sixth International
Workshop on Designing Correct Circuits: Vienna, 25-26 March 2006:
Participants' Proceedings. ETAPS 2006, March 2006.
A Satellite Event of the ETAPS 2006 group of conferences. [ bib | .pdf ] |
| [52] |
Mary Sheeran and Tom Melham, editors.
Sixth International Workshop on Designing Correct
Circuits: Vienna, 25-26 March 2006: Participants' Proceedings. ETAPS
2006, March 2006.
A Satellite Event of the ETAPS 2006 group of conferences. [ bib | .pdf ] |
| [53] |
Tom Melham and Mary Sheeran, editors.
Fifth International Workshop on Designing Correct
Circuits: Barcelona, 27-28 March 2004: Participants' Proceedings.
ETAPS 2004, March 2004.
A Satellite Event of the ETAPS 2004 group of conferences. [ bib | .pdf ] |
| [54] |
Jim Grundy, Tom Melham, and John O'Leary.
A reflective functional language for hardware design and theorem
proving.
Research Report PRG-RR-03-16, Programming Research Group, Oxford
University Computing Laboratory, October 2003. [ bib | .pdf ] |
| [55] |
Mary Sheeran and Tom Melham, editors.
Designing Correct Circuits (DCC'02). ETAPS 2002, April 2002.
Proceedings of the Workshop on Designing Correct Circuits held
during 6-7 April 2002 in Grenoble, France. [ bib ] |
| [56] |
Mark D. Aagaard, Thomas F. Melham, and John W. O'Leary.
Xs are for trajectory evaluation, Booleans are for theorem
proving (extended version).
Technical Report TR-2000-52, Department of Computing Science,
University of Glasgow, January 2000. [ bib | .pdf ] |
| [57] |
Kong Woei Susanto and Tom Melham.
Formally analysed dynamic synthesis of hardware.
In Jim Grundy and Malcolm Newey, editors, Theorem Proving in
Higher Order Logics: Emerging Trends: 11th International Conference,
TPHOLs'98, Canberra, September 27 - October 1, 1998: Supplementary
Proceedings, pages 105-117. Australian National University, 1998. [ bib ] |
| [58] |
Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas.
ITP project anthology.
Technical Report TR-1997-36, Department of Computing Science,
University of Glasgow, November 1997. [ bib ] |
| [59] |
Tom F. Melham.
Some research issues in higher order logic theorem proving.
BRICS Notes Series NS-96-7, Department of Computer Science,
University of Aarhus, October 1996. [ bib ] |
| [60] |
Stuart Aitken, Philip Gray, Tom Melham, and Muffy Thomas.
A study of user activity in interactive theorem proving.
In Chris Johnson, editor, Task Centred Approaches To Interface
Design: Glasgow Interactive Systems Group Research Review, pages 195-218.
Department of Computing Science, University of Glasgow, August 1995.
GIST Technical Report G95.2. [ bib ] |
| [61] |
Tom Melham and Juanito Camilleri, editors.
Supplementary Proceedings of the 7th International Workshop on
Higher Order Logic Theorem Proving and its Applications. University of
Malta, September 1994. [ bib ] |
| [62] |
Juanito Camilleri and Tom Melham.
Reasoning with inductively defined relations in the HOL theorem
prover.
Technical Report 265, Computer Laboratory, University of Cambridge,
August 1992. [ bib | .pdf ] |
| [63] |
T. F. Melham.
A mechanized theory of the pi-calculus in HOL.
Technical Report 244, Computer Laboratory, University of Cambridge,
January 1992. [ bib ] |
| [64] |
T. F. Melham.
The HOL finite_sets Library.
Computer Laboratory, University of Cambridge, February 1992. [ bib ] |
| [65] |
T. F. Melham.
The HOL pred_sets Library.
Computer Laboratory, University of Cambridge, February 1992. [ bib ] |
| [66] |
T. F. Melham.
The HOL sets Library.
Computer Laboratory, University of Cambridge, October 1991. [ bib ] |
| [67] |
T. F. Melham.
The HOL string Library.
Computer Laboratory, University of Cambridge, June 1991. [ bib ] |
| [68] |
Graham Birtwistle, Brian Graham, Tom Melham, and Rick Schediwy.
Hardware verification by formal proof.
Research Report 88/328/40, Department of Computer Science, University
of Calgary, October 1988. [ bib ] |
| [69] |
Thomas F. Melham.
Automating recursive type definitions in higher order logic.
Technical Report 146, Computer Laboratory, University of Cambridge,
September 1988. [ bib ] |
| [70] |
Thomas F. Melham.
Using recursive types to reason about hardware in higher order logic.
Technical Report 135, Computer Laboratory, University of Cambridge,
May 1988. [ bib ] |
| [71] |
Thomas F. Melham.
Abstraction mechanisms for hardware verification.
Technical Report 106, Computer Laboratory, University of Cambridge,
May 1987. [ bib ] |
| [72] |
Albert Camilleri, Mike Gordon, and Tom Melham.
Hardware verification using higher-order logic.
Technical Report 91, Computer Laboratory, University of Cambridge,
June 1986. [ bib ] |
| [73] |
Graham Birtwistle, Jeff Joyce, Breen Liblong, Tom Melham, and Rick Schediwy.
Specification and VLSI design.
Research Report 85/220/33, Department of Computer Science, University
of Calgary, November 1985. [ bib ] |
| [74] |
Breen Liblong, Tom Melham, Graham Birtwistle, and John Kendall.
Towards a VLSI design tool system.
Research Report 84/175/33, Department of Computer Science, University
of Calgary, November 1984. [ bib ] |
| [75] |
Graham Birtwistle, David Hill, John Kendall, Bill Coates, Richard Esau, Wallace
Kroeker, Breen Liblong, Erwin Liu, Tom Melham, and Rick Schediwy.
EDICT: An environment for design using integrated circuit tools.
Research Report 84/155/13, Department of Computer Science, University
of Calgary, June 1984. [ bib ] |