Publications – Programming Languages and Systems Research Group

Below is a list of selected publications of the research group. A more detailed list of members’ publications can be found on the Kent Academic Repository (KAR) or on their individual staff profiles.

Alglave, J.; Batty, M.; Donaldson, A. F.; Gopalakrishnan, G.; Ketema, J.; Poetzl, D.; Sorensen, T.; Wickerson, J.(2015), ‘GPU Concurrency: Weak Behaviours and Programming Assumptions’. In: ACM SIGPLAN Notices. Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 577-591.
Bartoletti, M.; Bocchi, L.; Murgia, M.(2018), ‘Progress-preserving Refinements of CTA’. In: Leibniz International Proceedings in Informatics (LIPIcs). 1-19.
Bastian, T.;Kell, S.;Zappa Nardelli, F. (2019), ‘Reliable and Fast DWARF-Based Stack Unwinding’. Proceedings of the ACM on Programming Languages, 3.
Batty, M.;Donaldson, A. F. & Wickerson, J. (2016), ‘Overhauling SC atomics in C11 and OpenCL’. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 634-648.
Batty, M.; Memarian, K.; Nienhuis, K.; Pichon-Pharabod, J.; Sewell, P.(2015), ‘The Problem of Programming Language Concurrency Semantics’. In: Lecture Notes in Computer Science. 24th European Symposium on Programming, 9032. pp. 283-307.
Bereczky, D.;Thompson, S.; Horpacsi, D. (2020), ‘A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang’. In: Byrski, Aleksander and Hughes, John, eds. Trends in Functional Programming: 21st International Symposium, pp. 139-158.
Bocchi, L.(2017), ‘Timed Runtime Monitoring for Multiparty Conversations’. Formal Aspects of Computing, 29(5), pp. 877-910.
Bocchi, L.; Chen, T. C.; Demangeon, R.; Honda, K.; Yoshida, N.(2017), ‘Monitoring Networks through Multiparty Session Types’. Theoretical Computer Science 669. pp. 33-58.
Bocchi, L.; Yoshida, N.;Lange, J. (2015), ‘Meeting Deadlines Together’. In: Aceto, Luca and de Frutos-Escrig, David, eds. International Conference on Concurrency Theory (CONCUR). Leibniz International Proceedings in Informatics, pp. 283-296.
Bocchi, L.; Yang, W.;Yoshida, N. (2014), ‘Timed Multiparty Session Types’. In: Baldan, Paolo and Gorla, Daniele, eds. International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, pp. 419-434.
Bocchi, L.; Melgratti, H.;Tuosto, E. (2020), ‘On Resolving Non-determinism in Choreographies’. Logical Methods in Computer Science 16(3). 18:1-18:69.
Bruna, M.;Grigore, R.; Kiefer, S.; Ouaknine, J.; Worrell, J. (2016), ‘Proving the Herman-Protocol Conjecture’. In: Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide, eds. 43rd International Colloquium on Automata, Languages, and Programming.
Daloze, B.;Marr, S.; Bonetta, D.; Mössenböck, H. (2016), ‘Efficient and Thread-Safe Objects for Dynamically-Typed Languages’. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 642-659.
Daloze, B.;Tal, A.; Marr, S.; Mössenböck, H.; Petrank, E. (2018), ‘Parallelization of Dynamic Languages: Synchronizing Built-in Collections’. Proceedings of the ACM on Programming Languages, 2 (OOPSLA). Article Number 108.
Faddegon, M. & Chitil, O.(2016), ‘Lightweight Computation Tree Tracing for Lazy Functional Languages’. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 114-128.
Faddegon, M.& Chitil, O. (2015), ‘Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack’. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 33-42.
Grigore, R.(2017), ‘Java Generics are Turing Complete’. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 73-85.
Grigore, R.; Kiefer, S.(2018), ‘Selective Monitoring’. In: Leibniz International Proceedings in Informatics. 20.
Ivašković, A.; Mycroft, A. & Orchard, D.(2020), ‘Data-flow analyses as effects and graded monads’. In: Ariola, Zena M., ed. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics, 167.
Kell, S.(2016), ‘Dynamically Diagnosing Type Errors in Unsafe Code’. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, pp. 800-819.
Kell, S. (2020), ‘Convivial design heuristics for software systems’.Programming 144-148.
Kell, S.; Mulligan, D. P.; Sewell, P.(2016), ‘The Missing Link: Explaining ELF Static Linking, Semantically’. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 607-623.
Kumar, R.;Myreen, M. O.; Norrish, M. & Owens, S. (2014), ‘CakeML: A Verified Implementation of ML’. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179-191.
Lamela Seijas, P.; Nemish, A.; Smith, D. & Thompson, S.(2020), ‘Marlowe: Implementing and Analysing Financial Contracts on Blockchain’. In: Bernhard, Matthew and Bracciali, Andrea and Camp, L. Jean and Matsuo, Shin’ichiro and Maurushat, Alana and Rønne, Peter B. and Sala, Massimiliano, eds. Financial Cryptography and Data Security, pp. 496-511.
Lange, J.; Ng, N.; Toninho, B.; Yoshida, N.(2017), ‘Fencing off go: liveness and safety for channel-based programming’. In: Castagna, Giuseppe and Gordon, Andrew D., eds. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 748-761.
Lange, J.;Ng, N.; Toninho, B.; Yoshida, N. (2018), ‘A Static Verification Framework for Message Passing in Go using Behavioural Types’. In: Proceedings of the 40th International Conference on Software Engineering, pp. 1137-1148.
Lange, J.; Tuosto, E.; Yoshida, N.(2015), ‘From Communicating Machines to Graphical Choreographies’. In: ACM SIGPLAN NOTICES. POPL 2015 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 50(1), pp. 221-232.
Lange, J.; Yoshida, N.(2019), ‘Verifying Asynchronous Interactions via Communicating Session Automata’. In: Computer Aided Verification, pp. 97-117.
Lange, J.; Yoshida, N.(2017), ‘On the undecidability of asynchronous session subtyping’. In: Esparza, J. and Murawski, A., eds. Foundations of Software Science and Computation Structures, pp. 441-457.
Marr, S.;Ducasse, S. (2015), ‘Tracing vs. Partial Evaluation: Comparing Meta-Compilation Approaches for Self-Optimizing Interpreters’. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 821-839.
Marr, S.; Seaton, C.;Ducasse, S. (2015), ‘Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises’. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 545-554.
Memarian, K.;Gomes, V. B. F.; David, B.; Kell, S.; Richardson, A.; Watson, R. N. M.; Sewell, P. (2019), ‘Exploring C semantics and pointer provenance’. Proceedings of the ACM on Programming Languages, 3 (POPL). Article Number 67.
Mulligan, D. P.; Owens, S.;Gray, K. E.; Ridge, T.; Sewell, P. (2014), ‘Lem: reusable engineering of real-world semantics’. In: Proceedings of the 2014 ACM SIGPLAN International Conference on Functional Programming 49(9), pp. 175-188.
Okudono, T.& King, A. (2020), ‘Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic’. In: Biere, Armin and Parker, David, eds. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 79-96.
Orchard, D. A.; Contrastin, M.; Danish, M.; Rice, A.(2017), ‘Verifying Spatial Properties of Array Computations’. Journal of Proceedings of the ACM on Programming Languages, 1 (OOPSLA).
Orchard, D. A.; Liepelt, V.;Eades, H. (2019), ‘Quantitative program reasoning with graded modal types’. Proceedings of the ACM on Programming Languages, 3 (ICFP). Article Number 110.
Orchard, D. A.; Rice, A. C.; Oshmyan, O.(2015), ‘Evolving Fortran types with inferred units-of-measure’. Journal of Computational Science, 9, 156-162.
Orchard, D. A.& Yoshida, N. (2016), ‘Effects as Sessions, Sessions as Effects’. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 568-581.
Paviotti, M.;Cooksey, S.; Paradis, A.; Wright, D.; Owens, S.; Batty, M. (2020), ‘Modular Relaxed Dependencies in Weak Memory Concurrency’. In: Lecture Notes in Computer Science. Programming Languages and System: 29th European Symposium on Programming, pp. 599-625.
Petricek, T. (2017), ‘Data exploration through dot-driven development’. In: ECOOP 2017. 21:1-21:27.
Petricek, T. (2020), ‘Foundations of a live data exploration environment’.Art, Science, and Engineering of Programming 4(3): 8
Petricek, T.; Guerra, G. & Syme, D.(2016), ‘Types from Data: Making Structured Data First-class Citizens in F#’. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 477-490.
Petricek, T.; Orchard, D. A.& Mycroft, A. (2014), ‘Coeffects: A calculus of context-dependent computation’. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp. 123-135.
Ritson, C. G.; Ugawa, T.; Jones, R. E.(2014), ‘Exploring Garbage Collection with Haswell Hardware Transactional Memory’. In: ISMM ’14: Proceedings of the 2014 international symposium on Memory management, pp. 105-115.
Robbins, E.; King, A.;Howe, J. M. (2020), ‘Backjumping is Exception Handling’. Theory and Practice of Logic Programming, pp. 1-20.
Rowe, R.;Férée, H.; Thompson, S.; Owens, S. (2019), ‘Characterising Renaming within OCaml’s Module System: Theory and Implementation’. In: PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 950-965.
Seed, T.;King, A.; Evans, N.(2020), ‘Reducing Bit-Vector Polynomials to SAT using Gröbner Bases’. In: Pulina, Lusa and Martina, Seidl, eds. The 23rd International Conference on Theory and Applications of Satisfiability Testing, pp. 361-377.
Sharrad, J.& Chitil, O. (2020), ‘Scaling Up Delta Debugging of Type Errors’. In: Trends in Functional Programming: 21st International Symposium, (In press)
Smith, C. L.;Kahrs, S. (2016), ‘Non-omega-overlapping TRSs are UN’. In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), 22:1-22:17.
Tan, Y. K.;Myreen, M. O.; Kumar, R.; Fooks, A. R.; Owens, S.; Norrish, M. (2016), ‘A New Verified Compiler Backend for CakeML’. In: ICFP’16: ACM SIGPLAN International Conference on Functional Programming, pp. 60-73.
Thompson, S.; Li, H.;Baker, R.; Adams, S.; Trinder, P.; Chechina, N.; Papaspyrou, N.; Sagonas, K.; Aronis, S.; Bihari, E. and others (2017), ‘Scaling Reliably: Improving the Scalability of the Erlang Distributed Actor Platform’. ACM Transactions on Programming Languages and Systems, 39(4). Article Number 17.
Torres Lopez, C.;Gurdeep Singh, R.; Marr, S.; Gonzalez Boix, E.; Scholliers, C. (2019), ‘Multiverse Debugging: Non-deterministic Debugging for Non-deterministic Programs’. In: 33rd European Conference on Object-Oriented Programming, 15-19 July 2019, London, UK.
Tsushima, K.;Chitil, O.; Sharrad, J.(2020), ‘Type Debugging with Counter-Factual Type Error Messages Using an Existing Type Checker’. In: IFL 2019: Proceedings of the 31st Symposium on Implementation and Application of Functional Languages, (In press)
Ugawa, T.;Ritson, C. G.; Jones, R. E.(2018), ‘Transactional Sapphire: Lessons in High Performance, On-the-fly Garbage Collection’. ACM Transactions on Programming Languages and Systems, 40(4). Article Number 15.
Wickerson, J.;Batty, M.; Beckmann, B. M. & Donaldson, A. F. (2015), ‘Remote-scope Promotion: Clarified, Rectified, and Verified’. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 731-747.
Wickerson, J.;Batty, M.; Sorensen, T. & Constantinides, G. A. (2017), ‘Automatically Comparing Memory Consistency Models’. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 52(1), pp. 190-204.
Zhang, X.;Mangal, R.; Grigore, R.; Naik, M. & Yang, H. (2014), ‘On abstraction refinement for program analyses in Datalog’. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 239-248.