@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.cs.ox.ac.uk/tom.melham/pub/Melham-1993-HOL.html}
}
@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.cs.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}
}
@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}
}
@INPROCEEDINGS{Khasidashvili:2009:AGV,
AUTHOR = {Zurab Khasidashvili and Gavriel Gavrielov and Tom Melham},
TITLE = {Assume-Guarantee Validation for {STE} Properties within
an {SVA} Environment},
BOOKTITLE = {Proceedings of 9th International Conference: 2009
Formal Methods in Computer-Aided Design: {FMCAD} 2009},
EDITOR = {Armin Biere and Carl Pixley},
PUBLISHER = {IEEE},
YEAR = {2009},
PAGES = {108--115},
ISBN = {978-1-4244-4966-8},
DOI = {10.1109/FMCAD.2009.5351133},
URL = {http://www.cs.ox.ac.uk/tom.melham/pub/Khasidashvili-2009-AGV.pdf}
}
@INPROCEEDINGS{Boehm:2008:ARA,
AUTHOR = {Peter B{\"o}hm and Tom Melham},
TITLE = {A Refinement Approach to Design and Verification
of On-Chip Communication Protocols},
BOOKTITLE = {2008 Formal Methods in Computer Aided Design:
{P}ortland, {O}regon, {USA}:
17--20 {N}ovember 2008},
EDITOR = {Alessandro Cimatti and Robert B. Jones},
PUBLISHER = {IEEE},
YEAR = {2008},
PAGES = {136--143},
ISBN = {978-1-4244-2735-2},
DOI = {10.1109/FMCAD.2008.ECP.22},
URL = {http://www.cs.ox.ac.uk/tom.melham/pub/Boehm-2008-ARA.pdf}
}
@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.cs.ox.ac.uk/tom.melham/pub/Adams-2007-AAS.pdf}
}
@INPROCEEDINGS{Hanna:2007:EVC,
AUTHOR = {Ziyad Hanna and Tom Melham},
TITLE = {Early Validation of Computer Microarchitecture
with Algorithm Level Models},
BOOKTITLE = {Proceedings of ASM'07: The 14th International Abstract
State Machines Workshop},
EDITOR = {Andreas Prinz},
ISBN = {978-82-7117-627-3},
YEAR = {2007},
NOTE = {Published electronically},
URL = {http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2007-EVC.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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}
}
@INPROCEEDINGS{Hanna:2009:SEF,
AUTHOR = {Ziyad Hanna and Tom Melham},
TITLE = {A Symbolic Execution Framework for Algorithm-Level Modelling},
BOOKTITLE = {High Level Design Validation and Test Workshop, 2009.
HLDVT 2009.},
EDITOR = {Priyank Kalla and Prabhat Mishra},
PUBLISHER = {IEEE},
YEAR = {2009},
PAGES = {94--99},
ISBN = {978-1-4244-4823-4},
ISSN = {1552-6674},
DOI = {10.1109/HLDVT.2009.5340168},
URL = {http://www.cs.ox.ac.uk/tom.melham/pub/Hanna-2009-SEF.pdf}
}
@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.cs.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.cs.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.cs.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.cs.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.cs.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}
}
@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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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.cs.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}
}
Tom Melham,
last updated in April 2010.