Geoffrey Hamilton

Dr

Profile Photo
Dr. Geoff Hamilton graduated from the University of Stirling, Scotland with a first class honours degree in 1989. He was awarded a Ph.D. from the University of Stirling in 1993. Geoff joined the Computer Science Department in the University of Keele, England as a lecturer in 1993, and then moved to the School of Computer Applications, DCU in 1998, where he is currently an associate professor.

Book

Year Publication
1993 Hamilton, Geoffrey William (1993) Compile-time optimisation of store usage in lazy functional programs (PhD Thesis). : University of Stirling.

Peer Reviewed Journal

Year Publication
2021 Ben-Amram, Amir M.;Hamilton, Geoff (2021) 'TIGHT POLYNOMIAL BOUNDS FOR LOOP PROGRAMS IN POLYNOMIAL SPACE'. Logical Methods in Computer Science, 17 (4). [DOI]
2020 Ben-Amram A.M.;Hamilton G. (2020) 'Tight polynomial worst-case bounds for loop programs'. Logical Methods in Computer Science, 16 (2):4:1-4:39. [DOI]
2020 G.W. Hamilton (2020) 'Distilling Programs to Prove Termination'. Electronic Proceedings In Theoretical Computer Science, 320 :140-154. [Link] [DOI]
2018 V. Kannan and G.W. Hamilton (2018) 'Functional Program Transformation for Parallelisation Using Skeletons'. International Journal of Parallel Programming, 46 (1):152-172. [Link] [DOI]
2017 Hamilton G. (2017) 'Generating Loop Invariants for Program Verification by Transformation'. Electronic Proceedings In Theoretical Computer Science, 253 :36-53. [DOI]
2016 Hamilton G. (2016) 'Generating Counterexamples for Model Checking by Transformation'. Electronic Proceedings In Theoretical Computer Science, 216 :65-82. [DOI]
2016 Kannan V.;Hamilton G. (2016) 'Program Transformation to Identify List-Based Parallel Skeletons'. Electronic Proceedings In Theoretical Computer Science, 216 :118-136. [DOI]
2015 Hamilton G. (2015) 'Verifying Temporal Properties of Reactive Systems by Transformation'. Electronic Proceedings In Theoretical Computer Science, 199 :33-49. [DOI]
2014 Aziz B.;Hamilton G. (2014) 'Enforcing reputation constraints on business process workflows'. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications, 5 (1):101-121.
2014 Gugel, Alberto and Aziz, Benjamin and Hamilton, Geoff (2014) 'Revisiting the ban-modified andrew secure rpc protocol'. Journal of Internet Services and Applications, 4 (3):82-96.
2011 Aziz B.;Hamilton G. (2011) 'Verifying a delegation protocol for grid systems'. Future Generation Computer Systems, 27 (5):476-485. [DOI]
2007 Aziz, B;Hamilton, G (2007) 'Modelling and analysis of PKI-based systems using process calculi'. International Journal of Foundations of Computer Science, 18 :593-618.
2007 Hamilton G. (2007) 'Distilling Programs for Verification'. Electronic Notes in Theoretical Computer Science, 190 (4):17-32. [DOI]
2006 Hamilton G. (2006) 'Poitín: Distilling theorems from conjectures'. Electronic Notes in Theoretical Computer Science, 151 (1):143-160. [DOI]
2006 Hamilton, G.W. (2006) 'Higher order deforestation'. Fundamenta Informaticae, 69 . [Link]
2005 Aziz B.;Hamilton G.;Gray D. (2005) 'A Denotational Approach to the Static Analysis of Cryptographic Processes'. Electronic Notes in Theoretical Computer Science, 118 :19-36. [DOI]
2005 Aziz, B;Hamilton, G;Gray, D (2005) 'A static analysis of cryptographic processes: the denotational approach'. Journal of Logic and Algebraic Programming, 64 :285-320. [DOI]
2000 Hamilton, GW (2000) 'Composing Fair Objects'. 1 (3):134-144.
1998 Hamilton, G.W. (1998) 'Usage Counting Analysis for Lazy Functional Languages'. Information and Computation, 146 . [Link] [DOI]

Conference Publication

Year Publication
2022 G.W. Hamilton and B. Aziz (2022) LNCS 13768:109-123 Excommunication: Transforming Pi-Calculus Specifications to Remove Internal Communication [Link] https://doi.org/10.1007/978-3-031-22476-8_7
2022 G. W. Hamilton (2022) LNCS 13290: 113-134 The Next 700 Program Transformers [Link] https://doi.org/10.1007/978-3-030-98869-2_7
2020 G.W. Hamilton (2020) Eighth International Workshop on Verification and Program Transformation Distilling Programs to Prove Termination
2019 Ben-Amram A.;Hamilton G. (2019) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Tight Worst-Case Bounds for Polynomial Loop Programs [DOI]
2017 G.W. Hamilton (2017) Fifth International Workshop on Verification and Program Transformation Generating Loop Invariants for Program Verification by Transformation
2016 V. Kannan and G.W. Hamilton (2016) Proceedings of the Fifth International Workshop on Metacomputation Distilling New Data Types [Link]
2016 G.W. Hamilton (2016) Proceedings of the Fourth International Workshop on Verification and Program Transformation Generating Counterexamples for Model Checking by Transformation
2016 V. Kannan and G.W. Hamilton (2016) 9th International Symposium on High-Level Parallel Programming and Applications Functional Program Transformation for Parallelisation using Skeletons
2016 Kannan V.;Hamilton G. (2016) Proceedings - 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016 Program Transformation to Identify Parallel Skeletons [DOI]
2016 V. Kannan and G.W. Hamilton (2016) Proceedings of the Fourth International Workshop on Verification and Program Transformation Program Transformation to Identify List-Based Parallel Skeletons
2015 Jones N.;Hamilton G. (2015) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Asymptotic speedups, bisimulation and distillation (Work in progress) [DOI]
2015 Dever M.;Hamilton G. (2015) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Automatically partitioning data to facilitate the parallelization of functional programs [DOI]
2015 G.W. Hamilton (2015) Proceedings of the Third International Workshop on Verification and Program Transformation Verifying Temporal Properties of Reactive Systems by Transformation
2014 M. Dever and G.W. Hamilton (2014) Proceedings of the Fourth International Workshop on Metacomputation AutoPar: Automating the Parallelization of Functional Programs
2014 N.D. Jones and G.W. Hamilton (2014) Proceedings of the Fourth International Workshop on Metacomputation Towards Understanding Superlinear Speedup by Distillation
2014 Kannan, Venkatesh and Hamilton, GW (2014) Proceedings of the Fourth International Workshop on Metacomputation Extracting Data Parallel Computations from Distilled Programs
2014 G.W. Hamilton and Morten Heine Sørensen (2014) Proceedings of the Second International Workshop on Verification and Program Transformation Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem
2013 Aziz B.;Hamilton G. (2013) Proceedings - 2013 International Conference on Availability, Reliability and Security, ARES 2013 Reputation-controlled business process workflows [DOI]
2013 Hamilton, G.W. (2013) Proceedings of the First International Workshop on Verification and Program Transformation On the Termination of Higher-Order Positive Supercompilation
2012 Hamilton G.;Jones N. (2012) Conference Record of the Annual ACM Symposium on Principles of Programming Languages Distillation with labelled transition systems
2012 G. Mendel-Gleason and G.W. Hamilton (2012) Proceedings of the Third International Workshop on Metacomputation Development of the Productive Forces
2012 M. Dever and G.W. Hamilton (2012) Proceedings of Trends in Functional Programming Automating the Parallelization of Functional Programs
2012 Hamilton G.;Jones N. (2012) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Proving the correctness of unfold/fold program transformations using bisimulation [DOI]
2012 Jones, Neil D and Hamilton, Geoff W (2012) Proceedings of the Third International Workshop on Metacomputation Superlinear speedup by program transformation
2012 G.W. Hamilton (2012) Proceedings of the Third International Workshop on Metacomputation A Hierarchy of Program Transformers
2012 M. Dever and G.W. Hamilton (2012) Proceedings of the Third International Workshop on Metacomputation A Comparison of Program Transformation Systems
2010 G. Mendel-Gleason and G.W. Hamilton (2010) Proceedings of the Second International Workshop on Metacomputation Supercompilation and Normalisation by Evaluation
2010 G.W. Hamilton and G. Mendel-Gleason (2010) Proceedings of the Second International Workshop on Metacomputation A Graph-Based Definition of Distillation
2010 Mendel-Gleason, Gavin and Hamilton, GW (2010) Workshop on Partiality and Recursion in Interactive Theorem Provers Inhabitation of (Co)-inductive Types using Transition Systems
2010 Hamilton G. (2010) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Extracting the essence of distillation [DOI]
2009 Aziz B.;Hamilton G. (2009) Proceedings - 2009 3rd International Conference on Emerging Security Information, Systems and Technologies, SECURWARE 2009 Detecting man-in-the-middle attacks by precise timing [DOI]
2008 G.W. Hamilton and M.H. Kabir (2008) Proceedings of the First International Workshop on Metacomputation Constructing Programs From Metasystem Transition Proofs
2007 Kabir, MH and Hamilton, GW (2007) Proceedings of the Sixth International Workshop on First-Order Theorem Proving Extending Poit\in to Handle Explicit Quantification
2007 Hamilton G. (2007) Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation Distillation: Extracting the essence of programs [DOI]
2005 Aziz B.;Gray D.;Hamilton G. (2005) Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) A static analysis of PKI-based systems [DOI]
2005 Power B.;Hamilton G. (2005) Proceedings - Fifth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2005 Declassification: Transforming java programs to remove intermediate classes [DOI]
2004 Sinclair D.;Gray D.;Hamilton G. (2004) Second International Symposium on Automated Technology for Verification and Analysis Synthesising attacks on cryptographic protocols [DOI]
2004 Gray, David and Aziz, Benjamin and Hamilton, Geoff (2004) Proceedings of the International Workshop on Security Analysis of Systems: Formalism and Tools Spiky: A nominal calculus for modelling protocols that use pkis
2002 Aziz, Benjamin and Hamilton, Geoff (2002) Proceedings of The Second Workshop on Specification, Analysis and Verification for Emerging Technologies A privacy analysis for the pi-calculus: The denotational approach
2002 Hamilton, GW (2002) TRENDS IN FUNCTIONAL PROGRAMMING 3 Extending higher-order deforestation: Transforming programs to eliminate even more trees
2001 B. Power and G.W. Hamilton (2001) Proceedings of the Workshop on Intermediate Representation Engineering for the Java Virtual Machine Declassification: Transforming Java Programs to Remove Intermediate Classes
2001 B. Aziz, D. Gray, G.W. Hamilton, F. Oehl, J. Power and D. Sinclair (2001) Proceedings of the International Conference on Advances in Infrastructure for Electronic Business, Science, and Education on the Internet Implementing Protocol Verification for E-Commerce
2001 D. Gray, G.W. Hamilton, J. Power and D. Sinclair (2001) Proceedings of the 2nd Joint Workshop on Formal Specification of Computer-Based Systems A Specification of TCP/IP using Mixed Intuitionistic Linear Logic
2001 Aziz, Benjamin and Hamilton, Geoff W (2001) IWFM A Denotational Semantics for the Pi-Calculus
2000 Gibson, J Paul and Hamilton, Geoff W and M\'ery, Dominique (2000) FIW A Taxonomy for Triggered Interactions Using Fair Object Semantics
2000 Hamilton, GW and Gibson, J Paul and M\'ery, D (2000) Proceedings of the International Conference on Software Engineering Applied to Networking & Parallel/ Distributed Computing Composing fair objects
2000 D. Sinclair, J. Power, J.P. Gibson, D. Gray and G.W. Hamilton (2000) Proceedings of the International Workshop on Distributed System Validation and Verification Specifying and Verifying IP with Linear Logic
1999 D. Gray, G.W. Hamilton, D. Sinclair, J.P. Gibson and J. Power (1999) Proceedings of The Third Irish Workshop on Formal Methods Four Logics and a Protocol
1999 Gibson, Paul and Hamilton, Geoff and M\'ery, Dominique (1999) Proceedings of The First International Conference on Integrated Formal Methods Integration problems in telephone feature requirements
1996 Hamilton, G (1996) Proceedings of the Eighth International Symposium on Programming Languages, Implementations, Logics, and Programs Higher order deforestation
1995 Hamilton, Geoff W (1995) Proceedings of the 1995 International Workshop on Memory Management Compile-time garbage collection for lazy functional languages
1992 Hamilton, Geoff W and Jones, Simon B (1992) Proceedings of the 1991 Glasgow Workshop on Functional Programming Extending deforestation for first order functional programs
1992 Hamilton, GW (1992) Workshop on Static Analysis of Equational, Functional and Logic Programming Languages, BIGRE Volume 81-82 Sharing Analysis of Lazy First Order Functional Programs
1991 Hamilton, Geoff W and Jones, SB (1991) JTASPEFT/WSA Transforming Programs to Eliminate Intermediate Structures
1991 Hamilton, Geoff W and Jones, Simon Benedict (1991) Proceedings of the 1990 Glasgow Workshop on Functional Programming Compile-time garbage collection by necessity analysis

Editorial

Year Publication
2022 G.W. Hamilton, T. Kahsai and M. Proietti (2022) Electronic Proceedings in Theoretical Computer Science, EPTCS 373: Preface. ED [Link] [DOI]
2016 Hamilton G.;Lisitsa A.;Nemytykh A. (2016) Electronic Proceedings in Theoretical Computer Science, EPTCS: Preface. ED [DOI]

Other Publication

Year Publication
1998 Brereton, P.;Budgen, D.;Hamilton, G. (1998) Hypertext: The next maintenance mountain. [Link] [DOI]
Certain data included herein are derived from the © Web of Science (2022) of Clarivate. All rights reserved.

Research Interests

My early research work was in the areas of program analysis and program transformation. This included the first extension of the deforestation algorithm to higher-order languages. Similar techniques were then used in an extension of the positive supercompilation algorithm to higher-order languages. A new transformation algorithm called the distillation algorithm was then built on top of positive supercompilation. This is a major advance over previous approaches, and gives orders of magnitude improvement in both the time and space usage of the transformed programs over what can be achieved using deforestation or positive supercompilation.

A hierarchy of program transformers was then developed, where the transformer at each level is built on top of those at lower levels, and more powerful transformations are obtained as we move up through this hierarchy. It turns out that these transformers can be applied in many different areas including theorem proving, automatic program construction, verification, optimisation, termination checking, parallelisation, complexity analysis and energy efficient computing.