Task 3 Papers

[1] David Chisnall, Brooks Davis, Khilan Gudka, Alexandre Joannou, Robert N. M. Watson, David Brazdil, Jonathan Woodruff, A. Theodore Markettos, J. Edward Maste, Robert Norton, Stacey Son, Michael Roe, Simon W. Moore, Peter G. Neumann, and Ben Laurie. Sinking the Java security model into the C. In Proceedings of ASPLOS 2017: the 22nd ACM International Conference on Architectural Support for Programming Languages and Operating Systems, April 2017. [ bib | Abstract ]
[2] Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. Verified compilation of CakeML to multiple machine-code targets. In Yves Bertot and Viktor Vafeiadis, editors, Proc. CPP 2017: Certified Programs and Proofs. ACM, January 2017. [ bib | DOI | .pdf | Abstract ]
[3] Stephen Kell. Some were meant for C: the endurance of an unmanageable language. In Onward! 2017: Proceedings of the 2017 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2017, New York, NY, USA, 2017. ACM. [ bib | DOI | .pdf | Abstract ]
[4] Jeremy Yallop, David Sheets, and Anil Madhavapeddy. A modular foreign function interface. Science of Computer Programming, 2017. [ bib | DOI | http | .pdf | Abstract ]
[5] Stephen Kell. Dynamically diagnosing type errors in unsafe code. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[6] Stephen Kell, Dominic P. Mulligan, and Peter Sewell. The missing link: explaining ELF static linking, semantically. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[7] Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. An operational semantics for C/C++11 concurrency. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[8] Kayvan Memarian and Peter Sewell. Clarifying unspecified values (draft defect report or proposal for c2x). ISO SC22 WG14 N2089, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2089.htm, September 2016. [ bib ]
[9] Kayvan Memarian and Peter Sewell. Clarifying pointer provenance (draft defect report or proposal for c2x). ISO SC22 WG14 N2090, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2090.htm, September 2016. [ bib ]
[10] Kayvan Memarian and Peter Sewell. Clarifying trap representations (draft defect report or proposal for c2x). ISO SC22 WG14 N2091, http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2091.htm, September 2016. [ bib ]
[11] Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. A new verified compiler backend for CakeML. In Proc. ICFP 2016: International Conference on Functional Programming. ACM Press, September 2016. [ bib | DOI | .pdf | Abstract ]
[12] Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. Into the depths of C: elaborating the de facto standards. In PLDI 2016, June 2016. PLDI 2016 Distinguished Paper award. [ bib | .pdf | Abstract ]
[13] Kayvan Memarian and Peter Sewell. Clarifying the C memory object model. ISO SC22 WG14 N2012, http://www.cl.cam.ac.uk/~pes20/cerberus/notes64-wg14.html, March 2016. [ bib ]
[14] David Chisnall, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Peter Sewell, and Robert N. M. Watson. C memory object and value semantics: the space of de facto and ISO standards. ISO SC22 WG14 N2013, http://www.cl.cam.ac.uk/~pes20/cerberus/notes30.pdf, March 2016. [ bib ]
[15] Kayvan Memarian and Peter Sewell. What is C in practice? (Cerberus survey v2): Analysis of responses. ISO SC22 WG14 N2014, http://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html, March 2016. [ bib ]
[16] Kayvan Memarian and Peter Sewell. What is C in practice? (Cerberus survey v2): Analysis of responses - with comments. ISO SC22 WG14 N2015, http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt, March 2016. [ bib ]
[17] Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In POPL 2016: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 622-633, January 2016. [ bib | DOI | http | .pdf | Abstract ]
[18] Khilan Gudka, Robert N. M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann, and Alex Richardson. Clean Application Compartmentalization with SOAAP. In CCS 2015: Proceedings of the 22nd ACM Conference on Computer and Communications Security, October 2015. [ bib | .pdf | Abstract ]
[19] Stephen Kell. Towards a dynamic object model within Unix processes. In Onward! 2015: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Pittsburgh, PA, USA, pages 224-239, October 2015. [ bib | DOI | http | .pdf | Abstract ]
[20] Kayvan Memarian, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell. Cerberus: towards an executable semantics for sequential and concurrent C11, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[21] Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. The problem of programming language concurrency semantics. In ESOP 2015: Programming Languages and Systems - 24th European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015., pages 283-307, April 2015. [ bib | DOI | http | .pdf | Abstract ]
[22] David Chisnall, Colin Rothwell, Brooks Davis, Robert N.M. Watson, Jonathan Woodruff, Munraj Vadera, Simon W. Moore, Peter G. Neumann, and Michael Roe. Beyond the PDP-11: Processor support for a memory-safe C abstract machine. In ASPLOS 2015: Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, ASPLOS XX, New York, NY, USA, March 2015. ACM. [ bib | DOI | .pdf | Abstract ]
[23] Mark John Batty. The C11 and C++11 Concurrency Model. PhD thesis, University of Cambridge Computer Laboratory, November 2014. Winner of 2015 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award and 2015 CPHC/BCS Distinguished Dissertation competition. [ bib ]
[24] Stephen Kell. In search of types. In Onward! 2014: Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2014, pages 227-241, New York, NY, USA, October 2014. ACM. [ bib | DOI | http | Abstract ]
[25] Reinoud Elhorst, Mark Batty, and David Chisnall. Efficient code generation for weakly ordered architectures. Presentation at the 4th European LLVM conference (EuroLLVM), April 2014. Slides and report available at http://llvm.org/devmtg/2014-04/. [ bib | Abstract ]
[26] Reinoud Elhorst. Lowering C11 atomics for ARM in LLVM, March 2014. [ bib | .pdf | Abstract ]
[27] Gabriel Kerneis, Charlie Shepherd, and Stefan Hajnoczi. QEMU/CPC: static analysis and CPS conversion for safe, portable, and efficient coroutines. In PEPM 2014: Proceedings of the ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation, San Diego, California, USA, pages 83-94, January 2014. [ bib | DOI | http | Abstract ]
[28] Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In POPL 2014: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, pages 179-192, January 2014. [ bib | DOI | http | Abstract ]
[29] Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program., 24(2-3):284-315, January 2014. [ bib | DOI | http | Abstract ]

This file was generated by bibtex2html 1.96.