School of Computing

Publications by Dr Scott Owens

Also view these in the Kent Academic Repository

Article
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). 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.
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.
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
Owens, S. et al. (2017). Verifying Efficient Function Calls in CakeML. in: ICFP 2017: 22nd ACM SIGPLAN International Conference on Functional Programming. ACM. Available at: http://icfp17.sigplan.org/home.
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.
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.
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.
Tan, Y., Owens, S. and Kumar, R. (2015). A Verified Type System for CakeML. in: Implementation and application of functional programming languages.
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.
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.
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: 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.
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.
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: ACM SIGPLAN Conference on Programming Language Design and Implementation,. ACM Press, pp. 311-322. Available at: http://doi.acm.org/10.1145/2254064.2254102.
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.
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.
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.
Weirich, S. et al. (2010). Ott or Nott. in: 5th ACM SIGPLAN Workshop on Mechanizing Metatheory.
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.
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 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.
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.
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.
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.
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: 29/06/2017