Geoffrey Hamilton
Dr
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.
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 |
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.