| Verifying higher-order functional programs with pattern-matching algebraic data types CHL Ong, SJ Ramsay ACM SIGPLAN Notices 46 (1), 587-598, 2011 | 142 | 2011 |
| A type-directed abstraction refinement approach to higher-order model checking SJ Ramsay, RP Neatherway, CHL Ong Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 75 | 2014 |
| A traversal-based algorithm for higher-order model checking RP Neatherway, SJ Ramsay, CHL Ong Proceedings of the 17th ACM SIGPLAN international conference on Functional …, 2012 | 51 | 2012 |
| Higher-order constrained horn clauses for verification T Cathcart Burn, CHL Ong, SJ Ramsay Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017 | 48 | 2017 |
| Model checking liveness properties of higher-order functional programs MM Lester, RP Neatherway, CHL Ong, S Ramsay | 19 | 2011 |
| Reachability in pushdown register automata AS Murawski, SJ Ramsay, N Tzevelekos Journal of Computer and System Sciences 87, 58-83, 2017 | 18 | 2017 |
| Bisimilarity in fresh-register automata AS Murawski, SJ Ramsay, N Tzevelekos Logical Methods in Computer Science 21, 2025 | 17 | 2025 |
| Game semantic analysis of equivalence in IMJ AS Murawski, SJ Ramsay, N Tzevelekos Automated Technology for Verification and Analysis: 13th International …, 2015 | 17 | 2015 |
| A Contextual Equivalence Checker for IMJ* AS Murawski, SJ Ramsay, N Tzevelekos Automated Technology for Verification and Analysis: 13th International …, 2015 | 14 | 2015 |
| Reachability in pushdown register automata AS Murawski, SJ Ramsay, N Tzevelekos International Symposium on Mathematical Foundations of Computer Science, 464-473, 2014 | 12 | 2014 |
| Polynomial-time equivalence testing for deterministic fresh-register automata A Murawski, S Ramsay, N Tzevelekos 43rd International Symposium on Mathematical Foundations of Computer Science …, 2018 | 11 | 2018 |
| Cycleq: an efficient basis for cyclic equational reasoning E Jones, CHL Ong, S Ramsay Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 9 | 2022 |
| Intensional datatype refinement: with application to scalable verification of pattern-match safety E Jones, S Ramsay Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021 | 5 | 2021 |
| Defunctionalization of higher-order constrained Horn clauses L Pham, SJ Ramsay, CHL Ong arXiv preprint arXiv:1810.03598, 2018 | 5 | 2018 |
| Intersection types and higer-order model checking S Ramsay, S Ramsay Oxford University, UK, 2014 | 5 | 2014 |
| Initial limit datalog: a new extensible class of decidable constrained horn clauses TC Burn, L Ong, S Ramsay, D Wagner 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021 | 4 | 2021 |
| Exact intersection type abstractions for safety checking of recursion schemes SJ Ramsay Proceedings of the 16th International Symposium on Principles and Practice …, 2014 | 4 | 2014 |
| Ill-Typed Programs Don’t Evaluate S Ramsay, C Walpole Proceedings of the ACM on Programming Languages 8 (POPL), 2010-2040, 2024 | 2 | 2024 |
| DEQ: equivalence checker for deterministic register automata AS Murawski, SJ Ramsay, N Tzevelekos Automated Technology for Verification and Analysis: 17th International …, 2019 | 2 | 2019 |
| Higher-order constrained horn clauses and refinement types TC Burn, CHL Ong, SJ Ramsay arXiv preprint arXiv:1705.06216, 2017 | 2 | 2017 |
Luke OngDistinguished University Professor, Nanyang Technological UniversityVerified email at ntu.edu.sg