Skip to main content Skip to navigation

Steven Ramsay

Research Fellow


steven
Now at the Oxford University Department of Computer Science.



Interests

I am broadly interested in programming languages and especially in program analysis for verification. During 08/13--10/15 I worked with Andrzej Murawski and Nikos Tzevelekos on the EPSRC funded project Game Semantics for Java Programs.



Publications


(PDF Document) A contextual equivalence checker for IMJ*. With Andrzej Murawski and Nikos Tzevelekos. To appear in Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA '15).

(PDF Document) Game semantic analysis of equivalence in IMJ. With Andrzej Murawski and Nikos Tzevelekos. To appear in Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA '15).
 
(PDF Document) Bisimilarity in fresh-register automata. With Andrzej Murawski and Nikos Tzevelekos. In Proceedings of the 13th ACM/IEEE Symposium on Logic in Computer Science (LICS '15).

(PDF Document) Reachability in pushdown register automata. With Andrzej Murawski and Nikos Tzevelekos. In Proceedings of the 39th International Symposium on the Mathematical Foundations of Computer Science (MFCS '14). Springer-Verlag.

(PDF Document) Exact intersection type abstractions for safety checking of recursion schemes. In Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP '14). ACM.

(PDF Document) A type-directed abstraction refinement approach to higher-order model checking. With Robin Neatherway and Luke Ong, in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, New York, NY, USA, 61-72

(PDF Document) Intersection types and higher-order model checking. DPhil thesis, University of Oxford, 2014.

(PDF Document) A traversal-based algorithm for higher-order model checking. With Robin Neatherway and Luke Ong, in Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP '12). ACM, New York, NY, USA, 353-364.

(PDF Document) Verifying higher-order functional programs with pattern-matching algebraic data types. With Luke Ong, in Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11). ACM, New York, NY, USA, 587-598.



Miscellaneous

In 2011, Chris Broadbent, Martin Lester, Robin Neatherway and I won the annual ACM-SIGPLAN ICFP Programming Contest. Martin has briefly documented our strategy here.

I am responsible for the higher-order model checker Preface, which can be downloaded from Luke Ong's group homepage in Oxford.