Verifying higher-order functional programs with pattern-matching algebraic data types. - C.-H. Luke Ong; Steven J. Ramsay (POPL, 2011)

A traversal-based algorithm for higher-order model checking. - Robin P. Neatherway; Steven J. Ramsay; C.-H. Luke Ong (ICFP, 2012)

A type-directed abstraction refinement approach to higher-order model checking. - Steven J. Ramsay; Robin P. Neatherway; C.-H. Luke Ong (POPL, 2014)

Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes. - Steven J. Ramsay (PPDP, 2014)

Intersection types and higer-order model checking. - Steven J. Ramsay (2014)

A Contextual Equivalence Checker for IMJ ∗. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (ATVA, 2015)

Game Semantic Analysis of Equivalence in IMJ. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (ATVA, 2015)

Higher-Order Constrained Horn Clauses and Refinement Types. - Toby Cathcart Burn; C.-H. Luke Ong; Steven J. Ramsay (CoRR, 2017)

Reachability in pushdown register automata. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (J. Comput. Syst. Sci., 2017)

Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (MFCS, 2018)

Defunctionalization of Higher-Order Constrained Horn Clauses. - Long Pham; Steven J. Ramsay; C.-H. Luke Ong (CoRR, 2018)

Higher-order constrained horn clauses for verification. - Toby Cathcart Burn; C.-H. Luke Ong; Steven J. Ramsay (Proc. ACM Program. Lang., 2018)

DEQ: Equivalence Checker for Deterministic Register Automata. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (ATVA, 2019)

Intensional Datatype Refinement. - Eddie Jones; Steven J. Ramsay (CoRR, 2020)

Verifying Liveness Properties of ML Programs. - Martin Lester 001; Robin P. Neatherway; C.-H. Luke Ong; Steven J. Ramsay (CoRR, 2020)

Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses. - Toby Cathcart Burn; Luke Ong; Steven J. Ramsay; Dominik Wagner 001 (LICS, 2021)

Intensional datatype refinement: with application to scalable verification of pattern-match safety. - Eddie Jones; Steven J. Ramsay (Proc. ACM Program. Lang., 2021)

CycleQ: an efficient basis for cyclic equational reasoning. - Eddie Jones; C.-H. Luke Ong; Steven J. Ramsay (PLDI, 2022)

Effect Handlers for Programmable Inference. - Minh Nguyen; Roly Perera; Meng Wang 002; Steven Ramsay (Haskell, 2023)

Effects and Effect Handlers for Programmable Inference. - Minh Nguyen; Roly Perera; Meng Wang 002; Steven Ramsay (CoRR, 2023)

Higher-Order MSL Horn Constraints. - Jerome Jochems; Eddie Jones; Steven J. Ramsay (Proc. ACM Program. Lang., 2023)

Ill-Typed Programs Don't Evaluate. - Steven Ramsay; Charlie Walpole (Proc. ACM Program. Lang., 2024)

Bisimilarity in fresh-register automata. - Andrzej S. Murawski; Steven J. Ramsay; Nikos Tzevelekos (Log. Methods Comput. Sci., 2025)