papers

Here is a list of my publications, in reverse chronological order.

• • Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. With Vasileios Koutavas and Yu-Yang Lin, in LICS: Proceedings 38th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, pp.1-13, 2023. DOI link. updated arXiv version

  • On-The-Fly Bisimilarity Checking for Fresh-Register Automata. With Hamza Bandukara, in SETTA: Dependable Software Engineering. Theories, Tools, and Applications. LNCS 13649, pp. 187-204, 2022. pdf

  • From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. With Vasileios Koutavas and Yu-Yang Lin, in TACAS: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, Part II. LNCS 13244, pp. 178-195, 2022. Springer (open access)

  • Theorems for Free from Separation Logic Specifications. With Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber and Kasper Svendsen, in Proceedings of the ACM on Programming Languages, Vol. 5, ICFP, Article 81, 29 pages, 2021. pdf

  • Game Semantics for Interface Middleweight Java. With Andrzej Murawski, extended version of POPL'14, in Journal of the ACM, Volume 68, Issue 1, ACM Press, 51 pages, 2020. pdf

  • Symbolic Execution Game Semantics. With Yu-Yang Lin, in FSCD'20: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, LIPIcs, pp. 27:1-27:42, 2020. link to publisher (open access)

  • A Bounded Model Checking Technique for Higher-Order Programs. With Yu-Yang Lin, in SETTA'19: Proceedings of the Symposium on Dependable Software Engineering, LNCS 11951, pp. 1-18, 2019. pdf

  • DEQ : Equivalence Checker for Deterministic Register Automata. With Andrzej Murawski and Steven Ramsay, in ATVA'19: 17th International Symposium on Automated Technology for Verification and Analysis, LNCS 11781, pp. 350-356, 2019. pdf

  • Higher-Order Linearisability. With Andrzej Murawski, extended version of CONCUR'17, in Journal of Logical and Algebraic Methods in Programming, Volume 104, pp. 86-116, 2019. link to publisher (open access)

  • Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. With Andrzej Murawski and Steven Ramsay, in MFCS'18: Proceedings of the 43rd International Symposium on Mathematical Foundations of Computer Science, LIPIcs, 72:1-72:14, 2018. link to publisher (open access)

  • A Trace Semantics for System F Parametric Polymorphism. With Guilhem Jaber, in FOSSACS'18: 21st International Conference on Foundations of Software Science and Computation Structures, LNCS 10803, in print. pdf

  • Algorithmic Games for Full Ground References. With Andrzej Murawski, extended version of ICALP'12, in Formal Methods in System Design, Volume 52, Issue 3, pp. 277-314, 2017. link to publisher (open access)

  • Reachability in Pushdown Register Automata. With Andrzej Murawski and Steven Ramsay, extended and upgraded version of MFCS'14, in Journal of Computer and System Sciences, pp. 58-83, 2017. link to publisher (free access)

  • Higher-Order Linearisability. With Andrzej Murawski, in CONCUR'17: 28th International Conference on Concurrency Theory, LIPIcs 85, pp.34:1-34:18. pdf

  • Block structure vs scope extrusion: between innocence and omniscience. With Andrzej Murawski, extended and upgraded version of FOSSACS'10, in Logical Methods in Computer Science, volume 12(3), 2016. link to pdf

  • Trace semantics for polymorphic references. With Guilhem Jaber, in LICS'16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 585-594, ACM, 2016. revised pdf

  • History-Register Automata. With Radu Grigore, extended and upgraded version of FOSSACS'13, in Logical Methods in Computer Science, volume 12(1), 2016. link to pdf

  • Nominal Game Semantics. With Andrzej Murawski, in Foundations and Trends in Programming Languages , volume 2(4), pp. 191-269, 2016. pdf

  • A Contextual Equivalence Checker for IMJ*. With Andrzej Murawski and Steven Ramsay, in ATVA'15: Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, LNCS, pp. 234-240, 2015. pdf

  • Game Semantic Analysis of Equivalence in IMJ. With Andrzej Murawski and Steven Ramsay, in ATVA'15: Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis, LNCS, pp. 411-428, 2015. pdf

  • Bisimilarity in Fresh-Register Automata. With Andrzej Murawski and Steven Ramsay, in LICS'15: Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, pp. 156-167, 2015. pdf

  • Reachability in Pushdown Register Automata. With Andrzej Murawski and Steven Ramsay, in MFCS'14: Proceedings of the 39th International Symposium on the Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 8634, pp. 464-473, 2014. pdf

  • Game Semantics for Nominal Exceptions. With Andrzej Murawski, in FoSSaCS'14: Proceedings of the 20th International Conference on Software Science and Computation Structures, Lecture Notes in Computer Science 8412, pp. 164-179, 2014. pdf

  • Game Semantics for Interface Middleweight Java. With Andrzej Murawski, in POPL'14: Proceedings of 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, pp. 517-528, 2014. pdf

  • Full Abstraction for Reduced ML. With Andrzej Murawski, in Annals of Pure and Applied Logic, 164(11), pp. 1118-1143, Elsevier, 2013. pdf

  • Towards Nominal Abramsky. With Andrzej Murawski, in Computation, Logic, Games, and Quantum Foundations: The Many Facets of Samson Abramsky, Lecture Notes in Computer Science 7860, pp. 246-263, 2013. pdf

  • History-Register Automata. With Radu Grigore, in FoSSaCS'13: Proceedings of the 19th International Conference on Software Science and Computation Structures, Lecture Notes in Computer Science 7794, pp. 17-33, 2013. pdf

  • Deconstructing general references via game semantics. With Andrzej Murawski, in FoSSaCS'13: Proceedings of the 19th International Conference on Software Science and Computation Structures, Lecture Notes in Computer Science 7794, pp. 241-256, 2013. pdf

  • Runtime Verification Based on Register Automata. With Radu Grigore, Dino Distefano and Rasmus L. Petersen, in TACAS'13: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 7795, pp. 260-276, 2013. pdf

  • Algorithmic Games for Full Ground References. With Andrzej Murawski, in ICALP'12: Proceedings of the 39th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 7392, pp. 312-324, 2012. pdf 

  • A System-Level Game Semantics. With Dan Ghica, in MFPS'12: Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics, pp. 191-211, 2012. pdf

  • Program equivalence in a simple language with state. In Computer Languages, Systems and Structures, Elsevier, volume 38(2), pp. 181-198, 2012. (journal version of Dagstuhl 10351) pdf 

  • Game semantics for good general references. With Andrzej Murawski, in LiCS'11: Proceedings of the 26th IEEE Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 75-84, 2011. pdf

  • Algorithmic Nominal Game Semantics. With Andrzej Murawski, in ESOP'11: Proceedings of the 20th European Symposium on Programming, Lecture Notes in Computer Science, Springer, volume 6602, pp. 419-438, 2011. pdf

  • Fresh-Register Automata. In POPL'11: Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, ACM Press, pp. 295-306, 2011. revised pdf

  • Introduction to  Category Theory and Categorical Logic. With Samson Abramsky, in New Structures for Physics, Lecture Notes in Physics, Springer, volume 813, pp. 3-94, 2011. link to pdf

  • Program Equivalence with Names. In Modelling, Controlling and Reasoning About State: Proceedings of Dagstuhl Seminar 10351, 2010. pdf

  • Block structure vs scope extrusion: between innocence and omniscience. With Andrzej Murawski, in FoSSaCS’10: Proceedings of the 13th International Conference on Foundations of Software Science and Computation Structures, LNCS 6014, pp. 33-47, 2010. pdf

  • Functional Reachability. With Luke Ong, in LiCS’09: Proceedings of the 24th IEEE Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 286-295, 2009. pdf

  • Full abstraction for Reduced ML. With Andrzej Murawski, in FoSSaCS’09: Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures, LNCS 5504, pp. 32-47, 2009. pdf

  • Nominal Game Semantics. PhD thesis, Oxford University Computing Laboratory, Trinity 2008. Available as Technical Report RR-09-18, OUCL, December 2009. pdf

  • Full abstraction for nominal general references. In Logical Methods in Computer Science, volume 5 (3:8), 2009. pdf

  • Full abstraction for nominal exceptions. Unpublished, 2008. pdf

  • Full abstraction for nominal general references. In LiCS’07: Proceedings of the 22nd IEEE Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 399-410, 2007. (Kleene best student paper award) revised pdf 

  • Investigations on the Dual Calculus. In Theoretical Computer Science 360(1-3): 289-326, 2006. pdf

  • Many-Valued Multiple-Expert modal models. In UNILOG’05: Proceedings of the First World Congress and School on Universal Logic, Polimetrica, pp. 351-364, 2005. pdf

  • An empirical local convergence study of alternative coordination schemes in analytical target cascading. With M. Kokkolaras, P.Y. Papalambros, M.F. Hulshof, L.F.P. Etman and J.E. Rooda, in Proceedings of the 5th World Congress on Structural and Multidisciplinary Optimization, 2003. pdf