School of Computing

Publications by Dr Scott Owens

Also view these in the Kent Academic Repository

Article
Owens, S. et al. (2017). Verifying Efficient Function Calls in CakeML. Proceedings of the ACM Programming Languages [Online] 1. Available at: http://icfp17.sigplan.org/home.
Kumar, R. et al. (2016). Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. Journal of Automated Reasoning [Online] 56:221-259. Available at: http://dx.doi.org/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 [Online] 24:284-315. Available at: http://dx.doi.org/10.1017/S0956796813000282.
Sewell, P. et al. (2010). x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Communications of the ACM [Online] 53:89-97. Available at: http://dx.doi.org/10.1145/1785414.1785443.
Sewell, P. et al. (2010). Ott: Effective Tool Support for the Working Semanticist. Journal of Functional Programming [Online] 20:71-122. Available at: http://dx.doi.org/10.1017/S0956796809990293.
Owens, S., Reppy, J. and Turon, A. (2009). Regular-expression Derivatives Re-examined. Journal of Functional Programming [Online] 19:173-190. Available at: http://dx.doi.org/10.1017/S0956796808007090.
Owens, S. and Slind, K. (2008). Adapting Functional Programs to Higher-Order Logic. Higher-Order and Symbolic Computation [Online] 21:377-409. Available at: http://dx.doi.org/10.1007/s10990-008-9038-0.
Slind, K. et al. (2007). Proof Producing Synthesis of Arithmetic and Cryptographic Hardware. Formal Aspects of Computing [Online] 19:343-362. Available at: http://dx.doi.org/10.1007/s00165-007-0028-5.
Gordon, M. et al. (2006). Automatic Formal Synthesis of Hardware from Higher Order Logic. Electronic Notes in Theoretical Computer Science [Online] 145:27-43. Available at: http://dx.doi.org/10.1016/j.entcs.2005.10.003.
Book section
Slind, K., Li, G. and Owens, S. (2010). Compiling Higher Order Logic by Proof. in: Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, pp. 193-220. Available at: http://dx.doi.org/10.1007/978-1-4419-1539-9_7.
Monograph
Batty, M. et al. (2010). Mathematizing C++ Concurrency: The Post-Rapperswil Model. ISO IEC JTC1/SC22/WG21. Available at: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf.
Owens, S., Sarkar, S. and Sewell, P. (2009). A Better x86 Memory Model: x86-TSO (Extended Version). University of Cambridge, Computer Laboratory. Available at: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-745.pdf.
Conference or workshop item
Ritson, C. and Owens, S. (2016). Benchmarking weak memory models. in: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming. ACM Press, pp. 24:1-24:11. Available at: http://dx.doi.org/10.1145/2851141.2851150.
Tan, Y. et al. (2016). A New Verified Compiler Backend for CakeML. in: International Conference on Functional Programming. pp. 60-73.
Owens, S. et al. (2016). Functional Big-step Semantics. in: European Symposium on Programming (ESOP). Springer. Available at: http://dx.doi.org/10.1007/978-3-662-49498-1_23.
Tan, Y., Owens, S. and Kumar, R. (2015). A Verified Type System for CakeML. in: Implementation and application of functional programming languages.
Little, C., Gray, K. and Owens, S. (2015). JSTyper: Type inference fo JavaScript. in: Implementation and application of functional programming languages.. Available at: http://ifl2015.wikidot.com.
Kumar, R. et al. (2014). HOL with Definitions: Semantics, Soundness, and a Verified Implementation. in: Fifth International Conference on Interactive Theorem Proving. Springer, pp. 308-324. Available at: http://dx.doi.org/10.1007/978-3-319-08970-6_20.
Kumar, R. et al. (2014). CakeML: A Verified Implementation of ML. in: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 179-191. Available at: http://doi.acm.org/10.1145/2535838.2535841.
Mulligan, D. et al. (2014). Lem: reusable engineering of real-world semantics. in: The 19th ACM SIGPLAN International Conference on Functional Programming. ACM Press. Available at: http://dx.doi.org/10.1145/2628136.2628143.
Myreen, M., Owens, S. and Kumar, R. (2013). Steps Towards Verified Implementations of HOL Light (Rough Diamond). in: Interactive Theorem Proving: Fourth International Conference. ITP 2013. Springer, pp. 490-495. Available at: http://dx.doi.org/10.1007/978-3-642-39634-2_38.
Sarkar, S. et al. (2012). Synchronising C/C++ and POWER. in: ACM SIGPLAN Conference on Programming Language Design and Implementation,. ACM Press, pp. 311-322. Available at: http://doi.acm.org/10.1145/2254064.2254102.
Myreen, M. and Owens, S. (2012). Proof-Producing Synthesis of ML from Higher-Order Logic. in: ICFP '12: 17th ACM SIGPLAN International Conference on Functional Programming. New York, N.Y.: ACM Press, pp. 115-126. Available at: http://dx.doi.org/10.1145/2364527.2364545.
Batty, M. et al. (2012). Clarifying and compiling C/C++ concurrency: from C++11 to POWER. in: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 509-520. Available at: http://doi.acm.org/10.1145/2103656.2103717.
Mador-Haim, S. et al. (2012). An Axiomatic Memory Model for POWER Multiprocessors. in: Computer Aided Verification, 24th International Conference, CAV 2012. Springer, pp. 495-512. Available at: http://dx.doi.org/10.1007/978-3-642-31424-7_36.
Sarkar, S. et al. (2012). Synchronising C/C++ and POWER. in: PLDI '12: 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, N.Y.: ACM Press, pp. 311-322. Available at: http://dx.doi.org/10.1145/2254064.2254102.
Batty, M. et al. (2012). Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER. in: POPL '12: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, N.Y.: ACM Press, pp. 509-520. Available at: http://dx.doi.org/10.1145/2103656.2103717.
Batty, M. et al. (2011). Mathematizing C++ concurrency. in: 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2011. ACM Press, pp. 55-66. Available at: http://doi.acm.org/10.1145/1926385.1926394.
Batty, M. et al. (2011). Mathematizing C++ Concurrency. in: Sagiv, M. ed. POPL '11: 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, N.Y.: ACM Press, pp. 55-66. Available at: http://dx.doi.org/10.1145/1926385.1926394.
Owens, S. et al. (2011). Lem: A Lightweight Tool for Heavyweight Semantics (Rough Diamond). in: Interactive Theorem Proving: Second International Conference, ITP 2011. Springer, pp. 363-369. Available at: http://dx.doi.org/10.1007/978-3-642-22863-6_27.
Blanchette, J. et al. (2011). Nitpicking C++ concurrency. in: Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. pp. 113-124. Available at: http://doi.acm.org/10.1145/2003476.2003493.
Blanchette, J. et al. (2011). Nitpicking C++ Concurrency. in: PPDP '11: Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. ACM Press, pp. 113-124. Available at: http://dx.doi.org/10.1145/2003476.2003493.
Weirich, S. et al. (2010). Ott or Nott. in: 5th ACM SIGPLAN Workshop on Mechanizing Metatheory.
Owens, S. (2010). Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. in: d'Hondt, T. ed. ECOOP 2010 - Object-Oriented Programming, 24th European Conference. Springer, pp. 478-503. Available at: http://dx.doi.org/10.1007/978-3-642-14107-2_23.
Zappa Nardelli, F. et al. (2009). Relaxed Memory Models Must Be Rigorous. in: Exploiting Concurrency Efficiently and Correctly, CAV 2009 Workshop.
Sarkar, S. et al. (2009). The Semantics of x86-CC Multiprocessor Machine Code. in: POPL '09: 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, N.Y.: ACM Press, pp. 379-391. Available at: http://dx.doi.org/10.1145/1480881.1480929.
Owens, S., Sarkar, S. and Sewell, P. (2009). A Better x86 Memory Model: x86-TSO. in: Berghofer, S. et al. eds. 22nd International Conference, TPHOLs 2009. Springer, pp. 391-407. Available at: http://dx.doi.org/10.1007/978-3-642-03359-9_27.
Owens, S. (2008). A Sound Semantics for OCaml light. in: Drossopoulou, S. ed. 17th European Symposium on Programming, ESOP 2008. Springer, pp. 1-15. Available at: http://dx.doi.org/10.1007/978-3-540-78739-6_1.
Owens, S. and Peskine, G. (2007). Verifying Type Soundness for OCaml: The Core Language. in: 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. in: Programming Languages and Systems: 16th European Symposium on Programming, ESOP 2007. Springer, pp. 205-219. Available at: http://dx.doi.org/10.1007/978-3-540-71316-6_15.
Sewell, P. et al. (2007). Ott: Effective Tool Support for the Working Semanticist. in: ICFP '07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming. ACM Press, pp. 1-12. Available at: http://dx.doi.org/10.1145/1291151.1291155.
Owens, S. and Flatt, M. (2006). From Structures and Functors to Modules and Units. in: ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming. ACM Press, pp. 87-98. Available at: http://dx.doi.org/10.1145/1159803.1159815.
Duan, J. et al. (2005). Functional Correctness Proofs of Encryption Algorithms. in: Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005. Springer-Verlag, pp. 519-533. Available at: http://dx.doi.org/10.1007/11591191_36.
Gordon, M. et al. (2005). A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic. in: Theorem Proving in Higher Order Logics: Emerging Trends Proceedings. Oxford University Computing Laboratory, pp. 59-75.
Culpepper, R., Owens, S. and Flatt, M. (2005). Syntactic Abstraction in Component Interfaces. in: Generative Programming and Component Engineering: 4th International Conference, GPCE 2005. Springer, pp. 373-388. Available at: http:/dx.doi.org/10.1007/11561347_25.
Owens, S. et al. (2004). Lexer and Parser Generators in Scheme. in: 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. in: User Interfaces for Theorem Provers: International Workshop UITP '03. Institut für Informatik, Albert-Ludwigs-Universität Freiburg, pp. 123-132.
Anshelevich, E. et al. (2000). Deformable Volumes in Path Planning Applications. in: IEEE International Conference on Robotics and Automation (ICRA). IEEE Press, pp. 2290-2295. Available at: http://dx.doi.org/10.1109/ROBOT.2000.846368.
Thesis
Owens, S. (2007). Compile-time Information in Software Components.
Total publications in KAR: 49 [See all in KAR]

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

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

Last Updated: 23/08/2017