Publications for ' no address book entry ' ordered by Year. (54)2003AMBAARM7 Formal Verification PlatformSusanto,K.W. Melham,T.F. To appear at the 5th International Conference on Formal Engineering Methods 2003. pp 20 Springer Verlag [More Details]. 2001Correct Hardware Design and Verification MethodsMargaria,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 1625 IEEE [More Details]. Formally Analyzed Dynamic Synthesis of Hardware Susanto,K.W. Melham,T.F. Journal of Supercomputing, vol 19, No 1 pp 722 [More Details]. 2000An Analysis of Errors in Interactive Proof AttemptsAitken,S. Melham,T.F. Interacting with Computers, Vol 12, No. 6. pp 565586 [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 7892 Springer Verlag [More Details]. A Methodology for LargeScale 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 ComputerAided Design). (Hunt, W.A. Jr and Johnson, S.D. Eds.). Lecture Notes in Computer Science, Volume No 1954 pp 263282 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]. 1999Xs are for Trajectory Evaluation, Booleans are for Theorem ProvingAagaard,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 202218 Springer [More Details]. 1998Formally Analysed Dynamic Synthesis of HardwareSusanto,K.W. Melham,T.F. The 11th International Conference TPHOL's '98  Supplementary Proceedings. pp 105117 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 263284 [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 308309 IEEE Computer Society Press [More Details]. 1996Some Research Issues in Higher Order Logic Theorem ProvingMelham,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 173190 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 18 University of York [More Details]. Some Research Issues in Higher Order Logic Theorem Proving Melham,T.F. volume NS967 Dept of Computer Science, University of Aarhus [More Details]. 1995A Study of User Activity in Interactive Theorem ProvingAitken,S. Gray,P. Melham,T.F. Thomas,M. Task Centred Approaches to Interface Design: Glasgow Interactive Systems Group Research Review pp 195218 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]. 1994Higher Order Logic Theorem Proving and Its ApplicationsMelham,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 picalculus in {HOL Melham,T.F. pp 5076 [More Details]. A Mechanized Theory of the picalculus in HOL Melham,T.F. Nordic Journal of Computing. Vol 1, no 1 pp 5076 [More Details]. he HOL Logic Extended with Quantification over Type Variables Melham,T.F. Journal: Formal Methods in System Design pp 724 [More Details]. The HOL Logic Extended with Quantification over Type Variables Melham,T.F. Journal: Formal Methods in System Design, vol3, no 12 pp 724 [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]. 1993The HOL Logic Extended with Quantification over Type VariablesMelham,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 A20 pp 317 NorthHolland [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 209229 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]. 1992A Mechanized Theory of the picalculus in {HOl}Melham,T.F. University of Cambridge [More Details]. The HOL predsets 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 350357 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 A10 NorthHolland [More Details]. 1991A Mechanized Theory of the picalculus in {HOL}Melham,T.F. Proceedings of the Second Workshop on Logical Frameworks pp 219237 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]. 1990Abstraction Mechanism for Hardware VerificationMelham,T.F. Formal Verification of Hardware Design pp 3049 IEEE Computer Society Press [More Details]. 1989Automatin Recursive Type Definitions in Higher Order LogisMelham,T.F. pp 341386 [More Details]. 1988Hardware Verification by Formal ProofBirtwistle,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 341386 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 2750 NorthHolland [More Details]. Abstraction Mechanism for Hardware Verification Melham,T.F. pp 267291 [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 379384 Canadian Society for Electrical Engineering [More Details]. 1987Abstraction Mechanisms for Hardware VerificationMelham,T.F. pp 267291 University of Cambridge [More Details]. 1986Hardware Verification using HigherOrder LogicCamilleri,A. Gordon,M. Melham,T.F. [More Details]. Hardware Verification Using HigherOrder 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 8397 [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 8397 NorthHolland [More Details]. 1985Specification and {VSLI} DesignBirtwistle,G. Joyce,J. Liblong,B. Melham,T.F. Schediwy,R. Computer Science, University of Calgary [More Details]. 1984Exploiting 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]. 
