School of Computing

Publications by Dr Scott Owens

Also view these in the Kent Academic Repository

Article
Tan, Y., Myreen, M., Kumar, R., Fox, A., Owens, S. and Norrish, M. (2019) "The Verified CakeML Compiler Backend", Journal of Functional Programming. Cambridge University Press. doi: 10.1017/S0956796818000229.
Owens, S., Norrish, M., Kumar, R., Myreen, M. and Tan, Y. (2017) "Verifying Efficient Function Calls in CakeML", Proceedings of the ACM Programming Languages. ICFP 2017: 22nd ACM SIGPLAN International Conference on Functional Programming, ACM. doi: 10.1145/3110262.
Kumar, R., Arthan, R., Myreen, M. and Owens, S. (2016) "Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation", Journal of Automated Reasoning. Springer, pp. 221-259. doi: 10.1007/s10817-015-9357-x.
Myreen, M. and Owens, S. (2014) "Proof-producing translation of higher-order logic into pure and stateful ML", Journal of Functional Programming. Cambridge University Press, pp. 284-315. doi: 10.1017/S0956796813000282.
Sewell, P., Sarkar, S., Owens, S., Zappa Nardelli, F. and Myreen, M. (2010) "x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors", Communications of the ACM, pp. 89-97. doi: 10.1145/1785414.1785443.
Sewell, P., Zappa Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S. and Strniša, R. (2010) "Ott: Effective Tool Support for the Working Semanticist", Journal of Functional Programming. Cambridge, pp. 71-122. doi: 10.1017/S0956796809990293.
Owens, S., Reppy, J. and Turon, A. (2009) "Regular-expression Derivatives Re-examined", Journal of Functional Programming, pp. 173-190. doi: 10.1017/S0956796808007090.
Owens, S. and Slind, K. (2008) "Adapting Functional Programs to Higher-Order Logic", Higher-Order and Symbolic Computation, pp. 377-409. doi: 10.1007/s10990-008-9038-0.
Slind, K., Owens, S., Iyoda, J. and Gordon, M. (2007) "Proof Producing Synthesis of Arithmetic and Cryptographic Hardware", Formal Aspects of Computing. Springer, pp. 343-362. doi: 10.1007/s00165-007-0028-5.
Gordon, M., Iyoda, J., Owens, S. and Slind, K. (2006) "Automatic Formal Synthesis of Hardware from Higher Order Logic", Electronic Notes in Theoretical Computer Science. Elsevier, pp. 27-43. doi: 10.1016/j.entcs.2005.10.003.
Book Section
Férée, H., Pohjola, J., Kumar, R., Owens, S., Myreen, M. and Ho, S. (2018) "Program Verification in the Presence of I/O". 10th International Conference on Verified Software: Theories, Tools, and Experiments, Springer. doi: 10.1007/978-3-030-03592-1_6.
"Benchmarking weak memory models" (2016). ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, New York, USA: ACM. doi: 10.1145/2851141.2851150.
Kumar, R., Myreen, M., Norrish, M. and Owens, S. (2014) "CakeML: A Verified Implementation of ML", Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, USA: ACM, pp. 179-191. doi: 10.1145/2535838.2535841.
Myreen, M., Owens, S. and Kumar, R. (2013) "Steps Towards Verified Implementations of HOL Light (Rough Diamond)", Interactive Theorem Proving: 4th International Conference, ITP 2013, Proceedings. Interactive Theorem Proving: Fourth International Conference. ITP 2013, Berlin, Germany: Springer, pp. 490-495. doi: 10.1007/978-3-642-39634-2_38.
Myreen, M. and Owens, S. (2012) "Proof-Producing Synthesis of ML from Higher-Order Logic", ICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming. ICFP '12: 17th ACM SIGPLAN International Conference on Functional Programming, New York, USA: ACM, pp. 115-126. doi: 10.1145/2364527.2364545.
Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M., Sewell, P. and Williams, D. (2012) "An Axiomatic Memory Model for POWER Multiprocessors", Computer Aided Verification. 24th International Conference, CAV 2012 Proceedings. Computer Aided Verification, 24th International Conference, CAV 2012, Berlin, Germany: Springer, pp. 495-512. doi: 10.1007/978-3-642-31424-7_36.
Batty, M., Memarian, K., Owens, S., Sarkar, S. and Sewell, P. (2012) "Clarifying and compiling C/C++ concurrency: from C++11 to POWER", ACM SIGPLAN Notices. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, USA: ACM, pp. 509-520. doi: 10.1145/2103656.2103717.
Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. and Williams, D. (2012) "Synchronising C/C++ and POWER", ACM SIGPLAN Notices. ACM SIGPLAN Conference on Programming Language Design and Implementation, New York, USA: ACM, pp. 311-322. doi: 10.1145/2254064.2254102.
Batty, M., Owens, S., Sarkar, S., Sewell, P. and Weber, T. (2011) "Mathematizing C++ concurrency", ACM SIGPLAN Notices. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2011, New York, USA: ACM, pp. 55-66. doi: 10.1145/1926385.1926394.
Blanchette, J., Weber, T., Batty, M., Owens, S. and Sarkar, S. (2011) "Nitpicking C++ concurrency", Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming. Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, New York, USA: ACM, pp. 113-124. doi: 10.1145/2003476.2003493.
Owens, S. (2010) "Reasoning about the Implementation of Concurrency Abstractions on x86-TSO", ECOOP 2010 – Object-Oriented Programming. Edited by T. d'Hondt. ECOOP 2010 —- Object-Oriented Programming, 24th European Conference, Berlin, Germany: Springer, pp. 478-503. doi: 10.1007/978-3-642-14107-2_23.
Slind, K., Li, G. and Owens, S. (2010) "Compiling Higher Order Logic by Proof". Springer, pp. 193-220. doi: 10.1007/978-1-4419-1539-9_7.
Owens, S., Sarkar, S. and Sewell, P. (2009) "A Better x86 Memory Model: x86-TSO", Theorem Proving in Higher Order Logics. Edited by S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel. 22nd International Conference, TPHOLs 2009, Berlin, Germany: Springer, pp. 391-407. doi: 10.1007/978-3-642-03359-9_27.
Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M. and Alglave, J. (2009) "The Semantics of x86-CC Multiprocessor Machine Code", POPL '09 Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL '09: 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, USA: ACM, pp. 379-391. doi: 10.1145/1480881.1480929.
Owens, S. (2008) "A Sound Semantics for OCaml\(_{light}\)", Programming Languages and Systems. Edited by S. Drossopoulou. 17th European Symposium on Programming, ESOP 2008, Berlin, Germany: Springer, pp. 1-15. doi: 10.1007/978-3-540-78739-6_1.
Anshelevich, E., Owens, S., Lamiraux, F. and Kavraki, L. (2000) "Deformable Volumes in Path Planning Applications", Proceedings - IEEE International Conference on Robotics and Automation. IEEE International Conference on Robotics and Automation (ICRA), IEEE, pp. 2290-2295. doi: 10.1109/ROBOT.2000.846368.
Conference Or Workshop Item
"Modular Relaxed Dependencies in Weak Memory Concurrency" (2020) Lecture Notes in Computer Science. 29th European Symposium on Programming, ESOP 2020, Springer, pp. 599-625. doi: 10.1007/978-3-030-44914-8_22.
Rowe, R., Férée, H., Thompson, S. and Owens, S. (2019) "Characterising Renaming within OCaml's Module System: Theory and Implementation", PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '19: ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM New York, NY, USA ©2019: ACM, pp. 950-965. doi: 10.1145/3314221.3314600.
Rowe, R., Férée, H., Thompson, S. and Owens, S. (2019) "ROTOR : A Tool for Renaming Values in OCaml's Module System", 2019 IEEE/ACM 3rd International Workshop on Refactoring (IWoR). 3rd International Workshop on Refactoring, IEEE Press, pp. 27-30. doi: 10.1109/IWoR.2019.00013.
Tan, Y., Myreen, M., Kumar, R., Fooks, A., Owens, S. and Norrish, M. (2016) "A New Verified Compiler Backend for CakeML". International Conference on Functional Programming, New York United States: Association for Computing Machinery, pp. 60-73. doi: 10.1145/2951913.2951924.
Owens, S., Myreen, M., Kumar, R. and Tan, Y. (2016) "Functional Big-step Semantics", Lecture Notes in Computer Science. European Symposium on Programming (ESOP), Springer. doi: 10.1007/978-3-662-49498-1_23.
Little, C., Gray, K. and Owens, S. (2015) "JSTyper: Type inference fo JavaScript". Implementation and application of functional programming languages. Available at: http://ifl2015.wikidot.com.
Tan, Y., Owens, S. and Kumar, R. (2015) "A Verified Type System for CakeML". Implementation and application of functional programming languages. doi: 10.1145/2897336.2897344.
Mulligan, D., Owens, S., Gray, K., Ridge, T. and Sewell, P. (2014) "Lem: reusable engineering of real-world semantics", ICFP'14 Proceedings of the 2014 ACM SIGPLAN International Conference on Functional Programming. The 19th ACM SIGPLAN International Conference on Functional Programming, ACM Press, pp. 175-188. doi: 10.1145/2628136.2628143.
Kumar, R., Arthan, R., Myreen, M. and Owens, S. (2014) "HOL with Definitions: Semantics, Soundness, and a Verified Implementation", Interactive Theorem Proving: Fifth International Conference, ITP 2014. Fifth International Conference on Interactive Theorem Proving, Springer, pp. 308-324. doi: 10.1007/978-3-319-08970-6_20.
Owens, S., Boehm, P., Zappa Nardelli, F. and Sewell, P. (2011) "Lem: A Lightweight Tool for Heavyweight Semantics (Rough Diamond)". Interactive Theorem Proving: Second International Conference, ITP 2011, Springer, pp. 363-369. doi: 10.1007/978-3-642-22863-6_27.
Blanchette, J., Weber, T., Batty, M., Owens, S. and Sarkar, S. (2011) "Nitpicking C++ Concurrency". PPDP '11: Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, ACM Press, pp. 113-124. doi: 10.1145/2003476.2003493.
Weirich, S., Owens, S., Sewell, P. and Zappa Nardelli, F. (2010) "Ott or Nott". 5th ACM SIGPLAN Workshop on Mechanizing Metatheory.
Rowe, R., Férée, H., Thompson, S. and Owens, S. (2009) "ROTOR: A Tool for Renaming Values in OCaml's Module System". 3rd International Workshop on Refactoring, IEEE. doi: 10.1109/IWoR.2019.00013.
Zappa Nardelli, F., Sewell, P., Sevcik, J., Sarkar, S., Owens, S., Maranget, L., Batty, M. and Alglave, J. (2009) "Relaxed Memory Models Must Be Rigorous". Exploiting Concurrency Efficiently and Correctly, CAV 2009 Workshop.
Sewell, P., Zappa Nardelli, F., Owens, S., Peskine, G., Ridge, T., Sarkar, S. and Strniša, R. (2007) "Ott: Effective Tool Support for the Working Semanticist". ICFP '07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, ACM Press, pp. 1-12. doi: 10.1145/1291151.1291155.
Owens, S. and Peskine, G. (2007) "Verifying Type Soundness for OCaml: The Core Language". 2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory.
Li, G., Owens, S. and Slind, K. (2007) "Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic". Programming Languages and Systems: 16th European Symposium on Programming, ESOP 2007, Springer, pp. 205-219. doi: 10.1007/978-3-540-71316-6_15.
Owens, S. and Flatt, M. (2006) "From Structures and Functors to Modules and Units". ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, ACM Press, pp. 87-98. doi: 10.1145/1159803.1159815.
Duan, J., Hurd, J., Li, G., Owens, S., Slind, K. and Zhang, J. (2005) "Functional Correctness Proofs of Encryption Algorithms". Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, Springer-Verlag, pp. 519-533. doi: 10.1007/11591191_36.
Culpepper, R., Owens, S. and Flatt, M. (2005) "Syntactic Abstraction in Component Interfaces". Generative Programming and Component Engineering: 4th International Conference, GPCE 2005, Springer, pp. 373-388. doi: 10.1007/11561347_25.
Gordon, M., Iyoda, J., Owens, S. and Slind, K. (2005) "A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic". Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, Oxford University Computing Laboratory, pp. 59-75.
Owens, S., Flatt, M., Shivers, O. and McMullan, B. (2004) "Lexer and Parser Generators in Scheme". Scheme 2004: Proceedings of the Fifth Workshop on Scheme and Functional Programming, Indiana University Department of Computer Science, pp. 41-52.
Owens, S. and Slind, K. (2003) "Proving as Programming with DrHOL: A Preliminary Design", Technical report 189. User Interfaces for Theorem Provers: International Workshop UITP '03, Institut für Informatik, Albert-Ludwigs-Universität Freiburg, pp. 123-132.
Monograph
Batty, M., Owens, S., Sarkar, S., Sewell, P. and Weber, T. (2010) "Mathematizing C++ Concurrency: The Post-Rapperswil Model". ISO IEC JTC1/SC22/WG21. doi: N3132.
Owens, S., Sarkar, S. and Sewell, P. (2009) "A Better x86 Memory Model: x86-TSO (Extended Version)". University of Cambridge, Computer Laboratory. doi: UCAM-CL-TR-745.
Thesis
Owens, S. (2007) "Compile-time Information in Software Components."
Total publications in KAR: 52 [See all in KAR]

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 02/12/2020