% ===================================================================== %% bibtex-file{ %% AUTHOR = "Professor Tom Melham", %% DATE = "Time-stamp: <08/06/03 10:40:07 melham>", %% FILENAME = "MelhamTF.bib", %% URL = "http://www.comlab.ox.ac.uk/tom.melham/pub/MelhamTF.bib", %% WWW-HOME = "http://www.comlab.ox.ac.uk/tom.melham/", %% ADDRESS = "Oxford University Computing Laboratory, %% Wolfson Building, Parks Road, %% Oxford, OX1 3QD, England", %% TELEPHONE = "+44 (0)1865 273824", %% FAX = "+44 (0)1865 273839", %% EMAIL = "Tom.Melham at comlab.ox.ac.uk", %% DATES = "1960--", %% SUPPORTED = "yes", %% SUPPORTED-BY = "Tom.Melham at comlab.ox.ac.uk", %% ABSTRACT = "Bibliography for the publications of Tom Melham."} % ===================================================================== % Books ---------------------------------------------------------------- @book{Melham:1993:HOL, AUTHOR = {T. Melham}, TITLE = {Higher Order Logic and Hardware Verification}, PUBLISHER = {Cambridge University Press}, YEAR = {1993}, SERIES = {Cambridge Tracts in Theoretical Computer Science}, VOLUME = {31}, ISBN = {0-521-41718-X}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-1993-HOL.html}} % Edited Books --------------------------------------------------------- @proceedings{Hurd:2005:TPH, EDITOR = {Joe Hurd and Tom Melham}, TITLE = {Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings}, BOOKTITLE = {Theorem Proving in Higher Order Logics: 18th International Conference, {TPHOLs} 2005: {O}xford, {UK}, {A}ugust 22--25, 2005: Proceedings}, PUBLISHER = {Springer-Verlag}, YEAR = {2005}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {3603}, ISBN = {3-540-28372-2}, ISSN = {0302-9743}, DOI = {10.1007/11541868}, URL = {http://www.springerlink.com/openurl.asp?genre=volume&id=doi:10.1007/11541868}} @proceedings{Margaria:2001:CHD, EDITOR = {Tiziana Margaria and Tom Melham}, TITLE = {Correct Hardware Design and Verification Methods: 11th {IFIP} {WG10.5} Advanced Research Working Conference, {CHARME} 2001: {L}ivingston, {S}cotland, {UK}, {S}eptember 4--7 2001: Proceedings}, BOOKTITLE = {Correct Hardware Design and Verification Methods: 11th {IFIP} {WG10.5} Advanced Research Working Conference, {CHARME} 2001: {L}ivingston, {S}cotland, {UK}, {S}eptember 4--7 2001: Proceedings}, PUBLISHER = {Springer-Verlag}, YEAR = {2001}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {2144}, ISBN = {3-540-42541-1}, ISSN = {0302-9743}, URL = {http://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=2144}} @proceedings{Melham:1994:HOL, EDITOR = {Thomas F. Melham and Juanito Camilleri}, TITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop: {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings}, BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, {V}alletta, {M}alta, {S}eptember 19--22, 1994: Proceedings}, PUBLISHER = {Springer-Verlag}, YEAR = {1994}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {859}, ISBN = {3-640-58450-1}} @book{Gordon:1993:ITH, EDITOR = {M. J. C. Gordon and T. F. Melham}, TITLE = {Introduction to {HOL}: A theorem proving environment for higher order logic}, PUBLISHER = {Cambridge University Press}, YEAR = {1993}, ISBN = {0-521-44189-7}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Gordon-1993-ITH.html}} @proceedings{Stavridou:1992:TPC, EDITOR = {V. Stavridou and T. F. Melham and R. T. Boute}, TITLE = {Theorem Provers in Circuit Design: Proceedings of the {IFIP} {TC}10/{WG} 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience: {N}ijmegen, {T}he {N}etherlands, 22--24 {J}une 1992}, BOOKTITLE = {Theorem Provers in Circuit Design: Proceedings of the {IFIP} {TC}10/{WG} 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice, and Experience: {N}ijmegen, {T}he {N}etherlands, 22--24 {J}une 1992}, PUBLISHER = {North-Holland}, YEAR = {1992}, SERIES = {IFIP Transactions A}, VOLUME = {10}, ISBN = {0-444-89686-4}, ISSN = {0926-5473}} % Dissertations ------------------------------------------------------- @phdthesis{Melham:1989:FAM, AUTHOR = {Thomas Frederick Melham}, TITLE = {Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic}, SCHOOL = {University of Cambridge}, MONTH = {August}, YEAR = {1989}} % Refereed Articles --------------------------------------------------- @inproceedings{Adams:2007:AAS, AUTHOR = {Sara Adams and Magnus Bj{\"o}rk and Tom Melham and Carl-Johan Seger}, TITLE = {Automatic Abstraction in Symbolic Trajectory Evaluation}, BOOKTITLE = {Formal Methods in Computer Aided Design: {FMCAD} 2007: {N}ovember 11--14 2007, {A}ustin, {T}exas, USA}, EDITOR = {Jason Baumgartner and Mary Sheeran}, PUBLISHER = {IEEE Computer Society}, YEAR = {2007}, PAGES = {127--135}, ISBN = {978-0-7695-3023-9}, DOI = {10.1109/.27}, URL = http://www.comlab.ox.ac.uk/tom.melham/pub/Adams-2007-AAS.pdf}} @article{Grundy:2006:RFL, AUTHOR = {Jim Grundy and Tom Melham and John O'Leary}, TITLE = {A Reflective Functional Language for Hardware Design and Theorem Proving}, JOURNAL = {Journal of Functional Programming}, VOLUME = {16}, NUMBER = {2}, MONTH = {March}, YEAR = {2006}, PAGES = {157--196}, ISSN = {0956-7968}, EISSN = {1469-7653}, DOI = {10.1017/S0956796805005757}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Grundy-2006-RFL.pdf}} @article{Grundy:2006:TBR, AUTHOR = {Jim Grundy and Tom Melham and Sava Krsti{\'c} and Sean McLaughlin}, TITLE = {Tool Building Requirements for an API to First-Order Solvers}, JOURNAL = {Electronic Notes in Theoretical Computer Science}, VOLUME = {144}, NUMBER = {2}, MONTH = {January}, YEAR = {2006}, PAGES = {15--26}, ISSN = {1571-0661}, DOI = {10.1016/j.entcs.2005.12.003}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Grundy-2006-TBR.pdf}} @article{Seger:2005:IEE, AUTHOR = {Carl-Johan H. Seger and Robert B. Jones and John W. O'Leary and Tom Melham and Mark D. Aagaard and Clark Barrett and Don Syme}, TITLE = {An Industrially Effective Environment for Formal Hardware Verification}, JOURNAL = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems}, VOLUME = {24}, NUMBER = {9}, MONTH = {September}, YEAR = {2005}, PAGES = {1381--1405}, ISSN = {0278-0070}, DOI = {10.1109/TCAD.2005.850814}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Seger-2005-IEE.pdf}} @inproceedings{Susanto:2003:AAF, AUTHOR = {Kong Woei Susanto and Tom Melham}, TITLE = {An {AMBA-ARM7} Formal Verification Platform}, BOOKTITLE = {Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, {ICFEM} 2003: {S}ingapore, {N}ovember 5--7, 2003: {P}roceedings}, EDITOR = {Jin Song Dong and Jim Woodcock}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {2885}, PUBLISHER = {Springer-Verlag}, YEAR = {2003}, PAGES = {48--67}, ISBN = {3-540-20461-X}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Susanto-2003-AAF.pdf}} @article{Dennis:2003:PT, AUTHOR = {Louise A. Dennis and Graham Collins and Michael Norrish and Richard J. Boulton and Konrad Slind and Thomas F. Melham}, TITLE = {The {PROSPER} toolkit}, JOURNAL = {International Journal on Software Tools for Technology Transfer}, VOLUME = {4}, NUMBER = {2}, YEAR = {2003}, MONTH = {February}, PAGES = {189--210}, ISSN = {1433-2787}, DOI = {10.1007/s100090200076}, URL = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/s100090200076}} @inproceedings{Melham:2002:ASI, AUTHOR = {Thomas F. Melham and Robert B. Jones}, TITLE = {Abstraction by Symbolic Indexing Transformations}, BOOKTITLE = {Formal Methods in Computer-Aided Design: 4th International Conference, {FMCAD} 2002: {P}ortland, {OR}, {USA}, {N}ovember 6--8, 2002: {P}roceedings}, EDITOR = {Mark D. Aagaard and John W. O'Leary}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {2517}, PUBLISHER = {Springer-Verlag}, YEAR = {2002}, PAGES = {1--18}, ISBN = {3-540-00116-6}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2002-ASI.pdf}} @article{Jones:2001:PFV, AUTHOR = {Robert B. Jones and John W. O'Leary and Carl-Johan H. Seger and Mark D. Aagaard and Thomas F. Melham}, TITLE = {Practical Formal Verification in Microprocessor Design}, JOURNAL = {{IEEE} Design {\&} Test of Computers}, VOLUME = {18}, NUMBER = {4}, MONTH = {July/August}, YEAR = {2001}, PAGES = {16--25}, ISSN = {0740-7475}, DOI = {10.1109/54.936245}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Jones-2001-PFV.pdf}} @article{Susanto:2001:FAD, AUTHOR = {Kong Woei Susanto and Tom Melham}, TITLE = {Formally Analyzed Dynamic Synthesis of Hardware}, JOURNAL = {The Journal of Supercomputing}, VOLUME = {19}, NUMBER = {1}, MONTH = {May}, YEAR = {2001}, PAGES = {7--22}, ISSN = {0920-8542}, DOI = {10.1023/A:1011132326153}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Susanto-2001-FAD.ps}} @inproceedings{Aagaard:2000:MLH, AUTHOR = {Mark D. Aagaard and Robert B. Jones and Thomas F. Melham and John W. O'Leary and Carl-Johan H. Seger}, TITLE = {A Methodology for Large-Scale Hardware Verification}, BOOKTITLE = {Formal Methods in Computer-Aided Design: Third International Conference, {FMCAD} 2000: {A}ustin, {TX}, {USA}, {N}ovember 1--3, 2000: {P}roceedings}, EDITOR = {Warren A. {Hunt, Jr.} and Steven D. Johnson}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1954}, PUBLISHER = {Springer-Verlag}, YEAR = {2000}, PAGES = {263--282}, ISBN = {3-540-41219-0}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Aagaard-2000-MLH.pdf}} @article{Aitken:2000:AEI, AUTHOR = {S. Aitken and T. Melham}, TITLE = {An analysis of errors in interactive proof attempts}, JOURNAL = {Interacting with Computers}, VOLUME = {12}, NUMBER = {6}, MONTH = {June}, YEAR = {2000}, PAGES = {565--586}, ISSN = {0953-5438}} @inproceedings{Dennis:2000:PT, AUTHOR = {Louise A. Dennis and Graham Collins and Michael Norrish and Richard Boulton and Konrad Slind and Graham Robinson and Mike Gordon and Tom Melham}, TITLE = {The {PROSPER} Toolkit}, BOOKTITLE = {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: {B}erlin, {G}ermany, {M}arch 25 -- {A}pril 2, 2000: {P}roceedings}, EDITOR = {Susanne Graf and Michael Schwartzbach}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1785}, PUBLISHER = {Springer-Verlag}, YEAR = {2000}, PAGES = {78--92}, ISBN = {3-540-67282-6}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Dennis-2000-PT.pdf}} @inproceedings{Aagaard:1999:XTE, AUTHOR = {Mark D. Aagaard and Thomas F. Melham and John W. O'Leary}, TITLE = {{X}s Are for Trajectory Evaluation, {B}ooleans Are for Theorem Proving}, BOOKTITLE = {Correct Hardware Design and Verification Methods: 10th {IFIP} {WG}10.5 Advanced Research Working Conference, {CHARME'99}: {B}ad {H}errenalb, {G}ermany, {S}eptember 27--29, 1999: {P}roceedings}, EDITOR = {Laurence Pierre and Thomas Kropf}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1703}, PUBLISHER = {Springer-Verlag}, YEAR = {1999}, PAGES = {202--218}, ISBN = {3-540-66559-5}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Aagaard-1999-XTE.pdf}} @inproceedings{McKay:1998:DSX, AUTHOR = {Nicholas McKay and Tom Melham and Kong Woei Susanto and Satnam Singh}, TITLE = {Dynamic Specialisation of {XC6200} {FPGA}s by Partial Evaluation}, BOOKTITLE = {Proceedings: {IEEE} Symposium on {FPGA}s for Custom Computing Machines: {A}pril 15--17, 1998, {N}apa {V}alley, {C}alifornia}, EDITOR = {Kenneth L. Pocek and Jeffrey M. Arnold}, PUBLISHER = {IEEE Computer Society}, YEAR = {1998}, PAGES = {308--309}, ISBN = {0-8186-8900-5}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/McKay-1998-DSX.pdf}} @article{Aitken:1998:ITP, AUTHOR = {J. S. Aitken and P. Gray and T. Melham and M. Thomas}, TITLE = {Interactive Theorem Proving: An Empirical Study of User Activity}, JOURNAL = {Journal of Symbolic Computation}, VOLUME = {25}, NUMBER = {2}, MONTH = {February}, YEAR = {1998}, PAGES = {263--284}, ISSN = {0747-7171}} @inproceedings{Gordon:1996:FAA, AUTHOR = {Andrew D. Gordon and Tom Melham}, TITLE = {Five Axioms of Alpha-Conversion}, BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference, {TPHOL}s'96: {T}urku, {F}inland, {A}ugust 26--30, 1996: Proceedings}, EDITOR = {J. von Wright and J. Grundy and J. Harrison}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1125}, PUBLISHER = {Springer-Verlag}, YEAR = {1996}, PAGES = {173--190}, ISBN = {3-540-61587-3}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Gordon-1996-FAA.pdf}} @inproceedings{Aitken:1996:PMI, AUTHOR = {J. S. Aitken and P. Gray and T. Melham and M. Thomas}, TITLE = {Phases, Modes and Information Flow in Theory Development}, BOOKTITLE = {User Interfaces for Theorem Provers: An International Workshop organised at the {D}epartment of {C}omputer {S}cience, {U}niversity of {Y}ork: 19th {J}uly 1996}, EDITOR = {Nicholas A. Merriam}, PUBLISHER = {University of York}, YEAR = {1996}, PAGES = {1--8}} @article{Melham:1994:MTP, AUTHOR = {T. F. Melham}, TITLE = {A Mechanized Theory of the {$\Pi$}-calculus in {HOL}}, JOURNAL = {Nordic Journal of Computing}, VOLUME = {1}, NUMBER = {1}, YEAR = {1994}, PAGES = {50--76}, ISSN = {1236-6064}} @article{Melham:1994:HLE, AUTHOR = {Thomas F. Melham}, TITLE = {The {HOL} Logic Extended with Quantification over Type Variables}, JOURNAL = {Formal Methods in System Design}, VOLUME = {3}, NUMBER = {1--2}, YEAR = {1994}, PAGES = {7--24}, ISSN = {0925-9856}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf}} @inproceedings{Melham:1993:HLE, AUTHOR = {Thomas F. Melham}, TITLE = {The {HOL} Logic Extended with Quantification over Type Variables}, BOOKTITLE = {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: {L}euven, {B}elgium, 21--24 {S}eptember 1992}, EDITOR = {Luc J. M. Claesen and Michael J. C. Gordon}, SERIES = {IFIP Transactions A}, VOLUME = {20}, PUBLISHER = {North-Holland}, YEAR = {1993}, PAGES = {3--17}, ISSN = {0926-5473}, ISBN = {0-444-89880-8}} @inproceedings{Jacobs:1993:TDT, AUTHOR = {Bart Jacobs and Tom Melham}, TITLE = {Translating Dependent Type Theory into Higher Order Logic}, BOOKTITLE = {Typed Lambda Calculi and Applications: International Conference on Typed Lamda Calculi and Applications: {TLCA '93}: {M}arch, 16--18, 1993, {U}trecht, {T}he {N}etherlands: Proceedings}, EDITOR = {M. Bezem and J. F. Groote}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {664}, PUBLISHER = {Springer-Verlag}, YEAR = {1993}, PAGES = {209--229}, ISBN = {3-540-56517-5}} @inproceedings{Melham:1992:PIR, AUTHOR = {T. F. Melham}, TITLE = {A Package for Inductive Relation Definitions in {HOL}}, BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem Proving System and its Applications, {D}avis, {C}alifornia, {A}ugust 28--30, 1991}, EDITOR = {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and Phillip J. Windley}, PUBLISHER = {IEEE Computer Society Press}, YEAR = {1992}, PAGES = {350--357}, ISBN = {0-8186-2460-4}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-1992-PIR.pdf}} @inproceedings{Melham:1988:URT, AUTHOR = {Thomas F. Melham}, TITLE = {Using Recursive Types to Reason about Hardware in Higher Order Logic}, BOOKTITLE = {The Fusion of Hardware Design and Verification: Proceedings of the {IFIP} {WG} 10.2 Working Conference on The Fusion of Hardware Design and Verification: {G}lasgow, {S}cotland, 4--6 {J}uly, 1988}, EDITOR = {George J. Milne}, PUBLISHER = {North-Holland}, YEAR = {1988}, PAGES = {27--50}, ISBN = {0-444-70532-5}} @inproceedings{Birtwistle:1988:HVF, AUTHOR = {G. Birtwistle and B. Graham and T. Melham and R. Schediwy}, TITLE = {Hardware Verification by Formal Proof}, BOOKTITLE = {Proceedings of the {C}anadian Conference on Electrical and Computer Engineering, {V}ancouver, {N}ovember 1988}, EDITOR = {V. K. Bhargava}, PUBLISHER = {Canadian Society for Electrical Engineering}, YEAR = {1988}, PAGES = {379--384}} @inproceedings{Camilleri:1987:HVH, AUTHOR = {Albert Camilleri and Mike Gordon and Tom Melham}, TITLE = {Hardware Verification using Higher-Order Logic}, BOOKTITLE = {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, {G}renoble, {F}rance, 9--11 {S}eptember, 1986}, EDITOR = {Dominique Borrione}, PUBLISHER = {North-Holland}, YEAR = {1987}, PAGES = {43--67}, ISBN = {0-444-70194-X}} @inproceedings{Birtwistle:1986:SVD, AUTHOR = {Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy}, TITLE = {Specification and {VLSI} Design}, BOOKTITLE = {Formal Aspects of {VLSI} Design: Proceedings of the 1985 {E}dinburgh Workshop on {VLSI}: {E}dinburgh, {S}cotland, {U.K.}}, EDITOR = {George J. Milne and P. A. Subrahmanyam}, PUBLISHER = {North-Holland}, YEAR = {1986}, PAGES = {83--97}, ISBN = {0-444-70026-9}} @article{Liblong:1985:TVD, AUTHOR = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, TITLE = {Towards a {VLSI} Design Tool System}, JOURNAL = {{INFOR}: Information Systems and Operational Research}, VOLUME = {23}, NUMBER = {4}, MONTH = {November}, YEAR = {1985}, PAGES = {389--402}, ISSN = {0315-5986}} @inproceedings{Liblong:1984:TVD, AUTHOR = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, TITLE = {Towards a {VLSI} Design Tool System}, BOOKTITLE = {{C}anadian Information Processing Society: {SESSION} 84: {P}roceedings}, EDITOR = {Leo Gotlieb}, PUBLISHER = {Canadian Information Processing Society}, PAGES = {37--42}, YEAR = {1984}, ISSN = {0825-5407}} @inproceedings{Liblong:1984:EHE, AUTHOR = {B. Liblong and T. Melham and G. Birtwistle}, TITLE = {Exploiting Hierarchies in {EDICT}}, BOOKTITLE = {Proceedings of the 1984 {C}anadian Conference on {VLSI}}, YEAR = {1984}} % Invited Articles ----------------------------------------------------- @inproceedings{Melham:2004:IMC, AUTHOR = {Tom Melham}, TITLE = {Integrating Model Checking and Theorem Proving in a Reflective Functional Language}, BOOKTITLE = {Integrated Formal Methods: 4th International Conference, {IFM} 2004: {C}anterbury, {UK}, {A}pril 4--7, 2004: Proceedings}, EDITOR = {Eerke A. Boiten and John Derrick and Graeme Smith}, PUBLISHER = {Springer-Verlag}, YEAR = {2004}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {2999}, PAGES = {36--39}, ISBN = {3-540-21377-5}, ISSN = {0302-9743}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2004-IMC.pdf}} @inproceedings{Melham:2003:AEP, AUTHOR = {Tom Melham}, TITLE = {Abstract: Experience with Practical Formal Verification at an Industrial Scale}, BOOKTITLE = {Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th--16th {A}pril 2003: {L}iverpool}, PAGES = {1--2}, YEAR = {2003}, ORGANIZATION = {Department of Computer Science, University of Liverpool}, EDITOR = {Clare Dixon}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2003-AEP.pdf}} @inproceedings{Melham:2002:PAI, AUTHOR = {Thomas F. Melham}, TITLE = {{PROSPER}: An Investigation into Software Architecture for Embedded Proof Engines}, BOOKTITLE = {Frontiers of Combining Systems: 4th International Workshop, {FroCoS} 2002: {S}anta {M}argherita {L}igure, {I}taly, {A}pril 8--10, 2002: Proceedings}, EDITOR = {Alessandro Armando}, PUBLISHER = {Springer-Verlag}, YEAR = {2002}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {2309}, PAGES = {193--206}, ISSN = {0302-9743}, ISBN = {3-540-43381-3}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2002-PAI.pdf}} @inproceedings{Aitken:1995:IPD, AUTHOR = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, TITLE = {Interactive Proof Discovery: An Empirical Study of {HOL} Users}, BOOKTITLE = {User Interface Design for Theorem Proving Systems: An International Workshop organised by the {ITP} Project}, EDITOR = {Philip Gray}, PUBLISHER = {Department of Computing Science, University of Glasgow}, YEAR = {1995}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Aitken-1995-IPD.pdf}} @inproceedings{Melham:1991:MTP, AUTHOR = {T. F. Melham}, TITLE = {A Mechanized Theory of the {$\pi$}-calculus in {HOL}}, BOOKTITLE = {Proceedings of the Second Workshop on Logical Frameworks}, EDITOR = {G. Huet and G. Plotkin}, PUBLISHER = {University of Edinburgh}, YEAR = {1991}, PAGES = {219--237}, NOTE = {Preliminary proceedings, published electronically after the workshop}} @incollection{Melham:1990:AMH, AUTHOR = {Thomas F. Melham}, TITLE = {Abstraction Mechanisms for Hardware Verification}, BOOKTITLE = {Formal Verification of Hardware Design}, EDITOR = {Michael Yoeli}, PUBLISHER = {IEEE Computer Society Press}, YEAR = {1990}, PAGES = {30--49}, ISBN = {0-8186-9017-8}} @incollection{Melham:1989:ART, AUTHOR = {Thomas F. Melham}, TITLE = {Automating Recursive Type Definitions in Higher Order Logic}, BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving}, EDITOR = {G. Birtwistle and P. A. Subrahmanyam}, PUBLISHER = {Springer-Verlag}, YEAR = {1989}, PAGES = {341--386}, ISBN = {0-387-96988-8}, ISBN = {3-540-96988-8}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-1989-ART.pdf}} @incollection{Melham:1988:AMH, AUTHOR = {Thomas F. Melham}, TITLE = {Abstraction Mechanisms for Hardware Verification}, BOOKTITLE = {{VLSI} Specification, Verification and Synthesis}, EDITOR = {Graham Birtwistle and P. A. Subrahmanyam}, PUBLISHER = {Kluwer Academic Publishers}, YEAR = {1988}, SERIES = {The Kluwer International Series in Engineeering and Computer Science}, VOLUME = {SECS35}, PAGES = {267--291}, ISBN = {0-89838-246-7}} % Research Reports and Other Publications ----------------------------- @techreport{Boehm:2008:DVOb, AUTHOR = {Peter B{\"o}hm and Tom Melham}, TITLE = {Design and Verification of On-Chip Communication Protocols}, YEAR = {2008}, MONTH = {April}, TYPE = {Research Report}, NUMBER = {RR-08-05}, INSTITUTION = {Oxford University Computing Laboratory}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOb.pdf}} @inproceedings{Boehm:2008:DVOa, AUTHOR = {Peter B{\"o}hm and Tom Melham}, TITLE = {Design and Verification of On-Chip Communication Protocols}, BOOKTITLE = {Seventh International Workshop on {D}esigning {C}orrect {C}ircuits: {B}udapest, 29--30 {M}arch 2008: Participants' Proceedings}, EDITOR = {Gordon J. Pace and Satnam Singh}, PUBLISHER = {ETAPS 2008}, NOTE = {A Satellite Event of the {ETAPS} 2008 group of conferences}, YEAR = {2008}, MONTH = {March}, PAGES = {15--29}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Boehm-2008-DVOa.pdf}} @inproceedings{Melham:2006:FHR, AUTHOR = {Tom Melham and John O'Leary}, TITLE = {A Functional {HDL} in Re{FL}ect}, BOOKTITLE = {Sixth International Workshop on {D}esigning {C}orrect {C}ircuits: {V}ienna, 25--26 {M}arch 2006: Participants' Proceedings}, EDITOR = {Mary Sheeran and Tom Melham}, PUBLISHER = {ETAPS 2006}, NOTE = {A Satellite Event of the {ETAPS} 2006 group of conferences}, YEAR = {2006}, MONTH = {March}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2006-FHR.pdf}} @proceedings{Sheeran:2006:FIW, EDITOR = {Mary Sheeran and Tom Melham}, TITLE = {Sixth International Workshop on {D}esigning {C}orrect {C}ircuits: {V}ienna, 25--26 {M}arch 2006: Participants' Proceedings}, PUBLISHER = {ETAPS 2006}, NOTE = {A Satellite Event of the {ETAPS} 2006 group of conferences}, YEAR = {2006}, MONTH = {March}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Sheeran-2006-FIW.pdf}} @proceedings{Melham:2004:FIW, EDITOR = {Tom Melham and Mary Sheeran}, TITLE = {Fifth International Workshop on {D}esigning {C}orrect {C}ircuits: {B}arcelona, 27--28 {M}arch 2004: Participants' Proceedings}, PUBLISHER = {ETAPS 2004}, NOTE = {A Satellite Event of the {ETAPS} 2004 group of conferences}, YEAR = {2004}, MONTH = {March}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-2004-FIW.pdf}} @techreport{Grundy:2003:RFL, AUTHOR = {Jim Grundy and Tom Melham and John O'Leary}, TITLE = {A Reflective Functional Language for Hardware Design and Theorem Proving}, NUMBER = {PRG-RR-03-16}, TYPE = {Research Report}, INSTITUTION = {Programming Research Group, Oxford University Computing Laboratory}, MONTH = {October}, YEAR = {2003}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Grundy-2003-RFL.pdf}} @proceedings{Sheeran:2002:DCC, EDITOR = {Mary Sheeran and Tom Melham}, TITLE = {Designing Correct Circuits ({DCC}'02)}, BOOKTITLE = {Designing Correct Circuits ({DCC}'02)}, PUBLISHER = {ETAPS 2002}, NOTE = {Proceedings of the Workshop on {D}esigning {C}orrect {C}ircuits held during 6--7 {A}pril 2002 in {G}renoble, {F}rance}, MONTH = {April}, YEAR = {2002}} @techreport{Aagaard:2000:XTE, AUTHOR = {Mark D. Aagaard and Thomas F. Melham and John W. O'Leary}, TITLE = {{X}s are for Trajectory Evaluation, {B}ooleans are for Theorem Proving (Extended Version)}, TYPE = {Technical Report}, NUMBER = {TR-2000-52}, INSTITUTION = {Department of Computing Science, University of Glasgow}, MONTH = {January}, YEAR = {2000}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Aagaard-2000-XTE.pdf}} @inproceedings{Susanto:1998:FAD, AUTHOR = {Kong Woei Susanto and Tom Melham}, TITLE = {Formally Analysed Dynamic Synthesis of Hardware}, BOOKTITLE = {Theorem Proving in Higher Order Logics: Emerging Trends: 11th International Conference, {TPHOL}s'98, {C}anberra, {S}eptember 27 -- {O}ctober 1, 1998: Supplementary Proceedings}, EDITOR = {Jim Grundy and Malcolm Newey}, PUBLISHER = {Australian National University}, YEAR = {1998}, PAGES = {105--117}, ISBN = {0-7315-4800-0}} @techreport{Aitken:1997:IPA, AUTHOR = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, TITLE = {{ITP} Project Anthology}, TYPE = {Technical Report}, NUMBER = {TR-1997-36}, INSTITUTION = {Department of Computing Science, University of Glasgow}, MONTH = {November}, YEAR = {1997}} @techreport{Melham:1996:SRI, AUTHOR = {Tom F. Melham}, TITLE = {Some Research Issues in Higher Order Logic Theorem Proving}, TYPE = {BRICS Notes Series}, NUMBER = {NS-96-7}, INSTITUTION = {Department of Computer Science, University of Aarhus}, MONTH = {October}, YEAR = {1996}, ISSN = {0909-3206}} @incollection{Aitken:1995:SUA, AUTHOR = {Stuart Aitken and Philip Gray and Tom Melham and Muffy Thomas}, TITLE = {A Study Of User Activity In Interactive Theorem Proving}, BOOKTITLE = {Task Centred Approaches To Interface Design: Glasgow Interactive Systems Group Research Review}, EDITOR = {Chris Johnson}, PUBLISHER = {Department of Computing Science, University of Glasgow}, NOTE = {GIST Technical Report G95.2}, MONTH = {August}, YEAR = {1995}, PAGES = {195--218}} @proceedings{Melham:1994:SPI, EDITOR = {Tom Melham and Juanito Camilleri}, TITLE = {Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications}, BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications}, PUBLISHER = {University of Malta}, MONTH = {September}, YEAR = {1994}} @techreport{Camilleri:1992:RID, AUTHOR = {Juanito Camilleri and Tom Melham}, TITLE = {Reasoning with Inductively Defined Relations in the {HOL} Theorem Prover}, TYPE = {Technical Report}, NUMBER = {265}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {August}, YEAR = {1992}, URL = {http://www.comlab.ox.ac.uk/tom.melham/pub/Camilleri-1992-RID.pdf}} @techreport{Melham:1992:MTP, AUTHOR = {T. F. Melham}, TITLE = {A Mechanized Theory of the {$\pi$}-calculus in {HOL}}, TYPE = {Technical Report}, NUMBER = {244}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {January}, YEAR = {1992}} @manual{Melham:1992:HFL, AUTHOR = {T. F. Melham}, TITLE = {The {HOL} finite\_sets Library}, ORGANIZATION = {Computer Laboratory, University of Cambridge}, MONTH = {February}, YEAR = {1992}} @manual{Melham:1992:HPL, AUTHOR = {T. F. Melham}, TITLE = {The {HOL} pred\_sets Library}, ORGANIZATION = {Computer Laboratory, University of Cambridge}, MONTH = {February}, YEAR = {1992}} @manual{Melham:1991:HSL, AUTHOR = {T. F. Melham}, TITLE = {The {HOL} sets Library}, ORGANIZATION = {Computer Laboratory, University of Cambridge}, MONTH = {October}, YEAR = {1991}} @manual{Melham:1991:HST, AUTHOR = {T. F. Melham}, TITLE = {The {HOL} string Library}, ORGANIZATION = {Computer Laboratory, University of Cambridge}, MONTH = {June}, YEAR = {1991}} @techreport{Birtwistle:1988:HVFP, AUTHOR = {Graham Birtwistle and Brian Graham and Tom Melham and Rick Schediwy }, TITLE = {Hardware Verification by Formal Proof}, TYPE = {Research Report}, NUMBER = {88/328/40}, INSTITUTION = {Department of Computer Science, University of Calgary}, MONTH = {October}, YEAR = {1988}} @techreport{Melham:1988:ART, AUTHOR = {Thomas F. Melham}, TITLE = {Automating Recursive Type Definitions in Higher Order Logic}, TYPE = {Technical Report}, NUMBER = {146}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {September}, YEAR = {1988}} @techreport{Melham:1988:RTR, AUTHOR = {Thomas F. Melham}, TITLE = {Using Recursive Types to Reason about Hardware in Higher Order Logic}, TYPE = {Technical Report}, NUMBER = {135}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {May}, YEAR = {1988}} @techreport{Melham:1987:AMH, AUTHOR = {Thomas F. Melham}, TITLE = {Abstraction Mechanisms for Hardware Verification}, TYPE = {Technical Report}, NUMBER = {106}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {May}, YEAR = {1987}} @techreport{Camilleri:1986:HVH, AUTHOR = {Albert Camilleri and Mike Gordon and Tom Melham}, TITLE = {Hardware Verification using Higher-Order Logic}, TYPE = {Technical Report}, NUMBER = {91}, INSTITUTION = {Computer Laboratory, University of Cambridge}, MONTH = {June}, YEAR = {1986}} @techreport{Birtwistle:1985:SVD, AUTHOR = {Graham Birtwistle and Jeff Joyce and Breen Liblong and Tom Melham and Rick Schediwy}, TITLE = {Specification and {VLSI} Design}, TYPE = {Research Report}, NUMBER = {85/220/33}, INSTITUTION = {Department of Computer Science, University of Calgary}, MONTH = {November}, YEAR = {1985}} @techreport{Liblong:1984:TAV, AUTHOR = {Breen Liblong and Tom Melham and Graham Birtwistle and John Kendall}, TITLE = {Towards a {VLSI} Design Tool System}, TYPE = {Research Report}, NUMBER = {84/175/33}, INSTITUTION = {Department of Computer Science, University of Calgary}, MONTH = {November}, YEAR = {1984}} @techreport{Birtwistle:1984:EED, AUTHOR = {Graham Birtwistle and David Hill and John Kendall and Bill Coates and Richard Esau and Wallace Kroeker and Breen Liblong and Erwin Liu and Tom Melham and Rick Schediwy}, TITLE = {{EDICT}: An Environment for Design Using Integrated Circuit Tools}, TYPE = {Research Report}, NUMBER = {84/155/13}, INSTITUTION = {Department of Computer Science, University of Calgary}, MONTH = {June}, YEAR = {1984}} % END ==================================================================