UNIVERSITY of GLASGOW

Computing at Glasgow University
 

Publications for '- no address book entry -' ordered by Year. (54)

2003 2001 2000 1999 1998 1996 1995 1994 1993 1992 1991 1990 1989 1988 1987 1986 1985 1984

2003

AMBA-ARM7 Formal Verification Platform
Susanto,K.W. Melham,T.F. To appear at the 5th International Conference on Formal Engineering Methods 2003. pp 20 Springer Verlag [More Details].

2001

Correct Hardware Design and Verification Methods
Margaria,T.
Melham,T.F. Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001: UK Springer Verlag [More Details].

Practical Formal Verification in Microprocessor Design
Jones,R.B. O'Leary,J.W. Seger,C.J.H. Aagaard,M.D. Melham,T.F. IEEE Design & Test of Computers, vol 18, No 4 pp 16-25 IEEE [More Details].

Formally Analyzed Dynamic Synthesis of Hardware
Susanto,K.W. Melham,T.F. Journal of Supercomputing, vol 19, No 1 pp 7-22 [More Details].

2000

An Analysis of Errors in Interactive Proof Attempts
Aitken,S.
Melham,T.F. Interacting with Computers, Vol 12, No. 6. pp 565-586 [More Details].

The PROSPER Toolkit
Dennis,L.A. Collins,G. Norrish,M. Boulton,R. Slind,K. Robinson,G. Gordon,M. Melham,T.F. Proceedings, Tools and Algorithms for the Construction and Analysis of Systems: 6th Intl. Conference, TACAS 2000, Berlin. (Graf, S. and Schwartzback, M. Eds.). Lecture Notes in Computer Science, Volume No 1785 pp 78-92 Springer Verlag [More Details].

A Methodology for Large-Scale Hardware Verification
Aagaard,M.D. Jones,R.B. O'Leary,J.W. Melham,T.F. Proceedings of 3rd Intl. Conference, FMCAD 2000, (Formal Methods in Computer-Aided Design). (Hunt, W.A. Jr and Johnson, S.D. Eds.). Lecture Notes in Computer Science, Volume No 1954 pp 263-282 Springer Verlag [More Details].

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving (Extended Version)
Aagaard,M.D. Melham,T.F. O'Leary,J.W. DCS Tech Report Dept of Computing Science, University of Glasgow [More Details].

1999

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving
Aagaard,M.D.
Melham,T.F. O'Leary,J.W. Proceedings of 10th IFIP WG10.5 Adv. Research Working Conference: Bad Herrenalb, Sep. 1999, (Pierre, L., Kropf, T. Eds.), Lecture Notes in Computer Science, Volume No. 1703. pp 202-218 Springer [More Details].

1998

Formally Analysed Dynamic Synthesis of Hardware
Susanto,K.W. Melham,T.F. The 11th International Conference TPHOL's '98 - Supplementary Proceedings. pp 105-117 Australian National University [More Details].

Interactive Theorem Proving: An Empirical Study of User Activity
Aitken,J.S. Gray,P. Melham,T.F. Thomas,M. Journal of Symbolic Computation. Volume No. 25 pp 263-284 [More Details].

Dynamic Specialisation of XC6200 FPGAs by Partial Evaluation
Mckay,N. Melham,T.F. Susanto,K.W. Singh,S. Proceedings of the IEEE Symposium on FPGAs for Custom Computing Machines pp 308-309 IEEE Computer Society Press [More Details].

1996

Some Research Issues in Higher Order Logic Theorem Proving
Melham,T.F. DCS Tech Report [More Details].

Five Axioms of Alpha Conversion
Gordon,A.D. Melham,T.F. Proceedings, Theorem Proving in Higher Order Logics: 9th Intl. Conference, TPHOL's '96. (von Wright, J. and Grudy J. and Harrison, L., Eds.). Lecture Notes in Computer Science, Volume No. 1125 pp 173-190 Springer [More Details].

Phases, Modes and Information Flow in Theory Development
Aitken,J.S. Gray,P. Melham,T.F. Thomas,M. An International Workshop:University of York pp 1-8 University of York [More Details].

Some Research Issues in Higher Order Logic Theorem Proving
Melham,T.F. volume NS-96-7 Dept of Computer Science, University of Aarhus [More Details].

1995

A Study of User Activity in Interactive Theorem Proving
Aitken,S. Gray,P.
Melham,T.F. Thomas,M. Task Centred Approaches to Interface Design: Glasgow Interactive Systems Group Research Review pp 195-218 Dept of Computing Science, University of Glasgow [More Details].

Interactive Proof Discover: An Empirical Study of HOL Users
Aitken,S. Gray,P. Melham,T.F. Thomas,M. User Interface Design for Theorem Proving Systems: an International Workshop University of Glasgow [More Details].

1994

Higher Order Logic Theorem Proving and Its Applications
Melham,T.F. Camilleri. J.,T.F. Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, Valletta, Malta, September 1994: Proceedings. Vol. 859 Springer [More Details].

A Mechanized Theory of the pi-calculus in {HOL
Melham,T.F. pp 50-76 [More Details].

A Mechanized Theory of the pi-calculus in HOL
Melham,T.F. Nordic Journal of Computing. Vol 1, no 1 pp 50-76 [More Details].

he HOL Logic Extended with Quantification over Type Variables
Melham,T.F. Journal: Formal Methods in System Design pp 7-24 [More Details].

The HOL Logic Extended with Quantification over Type Variables
Melham,T.F. Journal: Formal Methods in System Design, vol3, no 1-2 pp 7-24 [More Details].

Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications
Melham,T.F. Cammilleri,J. Proceedings of the 7th International Workshop on Higher Order Logice Theorem Proving and its Applications University of Malta [More Details].

1993

The HOL Logic Extended with Quantification over Type Variables
Melham,T.F. Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2, International Workshop, Leuven, September 1992. Series IFIP Transactions A-20 pp 3-17 North-Holland [More Details].

Translating Dependent Type Theory into Higher Order Logic
Jacobs,B. Melham,T.F. Typed Lambda Calculi and Applications: Proceedings of the International Conference, Utrecht, March 1993. Series, Lecture Notes in Computer Science. Vol 664 pp 209-229 Springer [More Details].

Introduction to HOL: A theorem proving environment for higher order logic
Melham,T.F. Gordon,M.J.C. Cambridge University Press [More Details].

1992

A Mechanized Theory of the pi-calculus in {HOl}
Melham,T.F. University of Cambridge [More Details].

The HOL pred-sets Library
Melham,T.F. University of Cambridge [More Details].

Reasoning with Inductively Defined Relations in the {HOL} Theorem Prover}
Camilleri,J. Melham,T.F. DCS Tech Report University of Cambridge [More Details].

A Mechanised Theory of the calculus in {HOl}}
Melham,T.F. [More Details].

The {HOL} finite\_sets Library
Melham,T.F. University of Cambridge [More Details].

A Package for Inductive Relation Definitions in {HOL}}
Melham,T.F. Proceedings of the 1991 International Workshopon the {HOL} Therom Proving System and its Applictions, Auguust 1991 pp 350-357 IEEE Computer Society Press [More Details].

Theorem Provers in Circuit Design
Stavridou,V. Melham,T.F. Boute,R.T. Proceedings of the IFIP TC10{WG 10.2 International Conference, Nijmegen, June 1992. Series IFIP Transactions A-10 North-Holland [More Details].

1991

A Mechanized Theory of the pi-calculus in {HOL}
Melham,T.F. Proceedings of the Second Workshop on Logical Frameworks pp 219-237 University of Edinburgh [More Details].

The HOL sets Library
Melham,T.F. University of Cambridge [More Details].

The HOL string Library
Melham,T.F. University of Cambridge [More Details].

1990

Abstraction Mechanism for Hardware Verification
Melham,T.F. Formal Verification of Hardware Design pp 30-49 IEEE Computer Society Press [More Details].

1989

Automatin Recursive Type Definitions in Higher Order Logis
Melham,T.F. pp 341-386 [More Details].

1988

Hardware Verification by Formal Proof
Birtwistle,G. Graham,B. Schediwy,R.
Melham,T.F. Computer Science, University of Calgary [More Details].

Automating Recursive Type Definitions in Higher Order Logic
Melham,T.F. Current Trends in Hardware Verficiation and Automated Theorem Proving pp 341-386 University of Cambridge [More Details].

Using Recursive Types to Reason about Hardware in Higerh Order Logic
Melham,T.F. Proceedings of the {IFIP} {WG} 10.2 Working Conference, Glasgow, July 1988 pp 27-50 North-Holland [More Details].

Abstraction Mechanism for Hardware Verification
Melham,T.F. pp 267-291 [More Details].

Using Recursive Types to Reason about Hardware in Higer Order Logic
Melham,T.F. University of Cambridge [More Details].

Hardware Verification by Formal Proof
Birtwistle,G. Graham,B. Melham,T.F. Schediwy,B. Proceedings of the Candadian Conference on Electrical and Computer Engineering pp 379-384 Canadian Society for Electrical Engineering [More Details].

1987

Abstraction Mechanisms for Hardware Verification
Melham,T.F. pp 267-291 University of Cambridge [More Details].

1986

Hardware Verification using Higher-Order Logic
Camilleri,A. Gordon,M.
Melham,T.F. [More Details].

Hardware Verification Using Higher-Order Logic
Camilleri,A. Gordon,M. Melham,T.F. University of Cambridge [More Details].

Specification and {VLSi} Design}
Birtwistle,G. Joyce,J. Liblong,B. Melham,T.F. Schediwy,R. pp 83-97 [More Details].

Specification and {VLSi} Design}
Birtwistle,G. Joyce,J. Liblong,B. Melham,T.F. Schediwy,R. Proceedings of the 1985 {E}dinburgh Workshop on {VSLI} pp 83-97 North-Holland [More Details].

1985

Specification and {VSLI} Design
Birtwistle,G. Joyce,J. Liblong,B.
Melham,T.F. Schediwy,R. Computer Science, University of Calgary [More Details].

1984

Exploiting Hierarchies in {EDICT}
Liblong,B.
Melham,T.F. Birtwistle.,T.F. Proceedings of the 1984 {C}anadian Conference on {VSLI} [More Details].

Towards a {VSLI} Design Tool System
Liblong,B. Melham,T.F. Birtwistle,G. Kendall,J. Computer Science, University of Calgary [More Details].

{{EDICT}: An Environment for Design Using Integrated Circuit Tools
Birtwistle,G. Hill,D. Kendall,J. Coates,B. Esau,R. Kroeker,W. Liblong,B. Liu,E. Melham,T.F. Schediwy,R. Computer Science, University of Calgary [More Details].