[1] Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. Efficient tagged memory. In ICCD 2017: IEEE 35th International Conference on Computer Design, November 2017. [ bib | DOI | www: | .pdf | Abstract ]
[2] Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic laws for weak consistency. In CONCUR 2017: Proceedings of 28th International Conference on Concurrency Theory, September 2017. [ bib | DOI | .html | Abstract ]
[3] 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 ]
[4] Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal. Caper: Automatic Verification for Fine-grained Concurrency. In Proc. ESOP 2017: 26th European Symposium on Programming, Lecture Notes in Computer Science. Springer, April 2017. [ bib | .pdf | Abstract ]
[5] Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. Abstract Specifications for Concurrent Maps. In Proc. ESOP 2017: 26th European Symposium on Programming, Lecture Notes in Computer Science. Springer, April 2017. [ bib | .pdf | Abstract ]
[6] Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 429-442, January 2017. [ bib | DOI | http | .pdf | Abstract ]
[7] 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 ]
[8] 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 ]
[9] Jeremy Yallop, David Sheets, and Anil Madhavapeddy. A modular foreign function interface. Science of Computer Programming, 2017. [ bib | DOI | http | .pdf | Abstract ]
[10] Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 218-231, New York, NY, USA, January 2017. ACM. [ bib | DOI | http | Abstract ]
[11] Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[12] Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[13] Azalea Raad. Abstraction, Refinement and Concurrent Reasoning. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[14] José Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva Naudziuniene. Towards logic-based verification of javascript programs. In Leonardo de Moura, editor, CADE 2017: Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 8-25. Springer, 2017. [ bib | DOI | .html ]
[15] Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying strong eventual consistency in distributed systems. In OOPSLA 2017: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2017. To appear. [ bib ]
[16] Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan. Programming and proving with classical types. In APLAS 2017: Proceedings of the 15th Asian Symposium on Programming Languages and Systems, 2017. To appear. [ bib ]
[17] Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Trace properties from separation logic specifications. CoRR, abs/1702.02972, 2017. [ bib | http | http | Abstract ]
[18] 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 ]
[19] 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 ]
[20] 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 ]
[21] Victor B. F. Gomes and Georg Struth. Modal Kleene algebra applied to program correctness. In John S. Fitzgerald, Stefania Gnesi, and Constance L. Heitmeyer, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Lecture Notes in Computer Science, pages 310-325. Springer, November 2016. [ bib | DOI | http | .pdf | Abstract ]
[22] Azalea Raad, Aquinas Hobor, Jules Villard, and Philippa Gardner. Verifying concurrent graph algorithms. In Proc. APLAS 2016: 14th Asian Symposium on Programming Languages and Systems, pages 314-334, November 2016. [ bib | DOI | http | Abstract ]
[23] Azalea Raad, José Fragoso Santos, and Philippa Gardner. DOM: specification and client reasoning. In Proc. APLAS 2016: 14th Asian Symposium on Programming Languages and Systems, pages 401-422, November 2016. [ bib | DOI | http | Abstract ]
[24] Brian Campbell and Ian Stark. Extracting behaviour from an executable instruction set model. In Ruzica Piskac and Muralidhar Talupur, editors, FMCAD 2016: Formal Methods in Computer-Aided Design, pages 33-40, October 2016. Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [ bib | .pdf | Abstract ]
[25] M. Naylor, S. W. Moore, and A. Mujumdar. A consistency checker for memory subsystem traces. In FMCAD 2016: Formal Methods in Computer-Aided Design, September 2016. [ bib | DOI | .pdf | Abstract ]
[26] Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Ed Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son, and Munraj Vadera. Fast protection-domain crossing in the CHERI capability-system architecture. IEEE Micro, 36(5):38-49, September 2016. [ bib | DOI | http | Abstract ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] Hannes Mehnert and Louis Gesbert. Conex - establishing trust into data repositories. In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[32] Enguerrand Decorne, Jeremy Yallop, and David Meršinjak. Ocaml inside: a drop-in replacement for libtls (extended abstract). In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[33] Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:15, Dagstuhl, Germany, August 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [ bib | DOI | .pdf | Abstract ]
[34] 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 ]
[35] Victor B. F. Gomes and Georg Struth. Program construction and verification components based on Kleene algebra. Archive of Formal Proofs, 2016, June 2016. [ bib | http | Abstract ]
[36] Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. Modular termination verification for non-blocking concurrency. In ESOP 2016: Proceedings of the 25th European Symposium on Programming, pages 176-201, April 2016. [ bib | DOI | http | .pdf | Abstract ]
[37] Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. Transfinite step-indexing: Decoupling concrete and logical steps. In ESOP 2016, pages 727-751, April 2016. [ bib | DOI | http | .pdf | Abstract ]
[38] Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, and Tjark Weber. Kleene algebras with domain. Archive of Formal Proofs, 2016, April 2016. [ bib | http | Abstract ]
[39] Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. Sci. Comput. Program., 118:60-76, March 2016. [ bib | DOI | .pdf | Abstract ]
[40] 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 ]
[41] 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 ]
[42] 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 ]
[43] 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 ]
[44] David Kaloper-Meršinjak and Hannes Mehnert. Not-quite-so-broken TLS 1.3 mechanised conformance checking. In TLSv1.3 - Ready or Not? (TRON) workshop, February 2016. [ bib | .pdf | Abstract ]
[45] Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In POPL 2016: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, pages 608-621, January 2016. [ bib | DOI | http | .pdf | Abstract ]
[46] 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 ]
[47] David Kaloper-Meršinjak and Jeremy Yallop. Generic partially-static data (extended abstract). In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pages 39-40, New York, NY, USA, 2016. ACM. [ bib | DOI | http | http | Abstract ]
[48] Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In MICRO 2015: Proceedings of the 48th International Symposium on Microarchitecture, , Waikiki, HI, USA, pages 635-646, December 2015. [ bib | DOI | http | .pdf | Abstract ]
[49] Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. Fault-tolerant Resource Reasoning. In APLAS 2015: Proceedings of the 13th Asian Symposium on Programming Languages and Systems, pages 169-188, December 2015. [ bib | DOI | http | .pdf | Abstract ]
[50] 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 ]
[51] 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 ]
[52] Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. In SOSP 2015: Proceedings of the 25th Symposium on Operating Systems Principles, Monterey, CA, USA, pages 38-53, October 2015. [ bib | DOI | http | .pdf | Abstract ]
[53] Gian Ntzik and Philippa Gardner. Reasoning about the POSIX File System: Local Update and Global Pathnames. In OOPSLA 2015: Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2015. [ bib | Abstract ]
[54] Matthew Naylor and Simon W. Moore. A generic synthesisable test bench. In MEMOCODE 2015: ACM/IEEE International Conference on Formal Methods and Models for Codesign, Austin, TX, USA, pages 128-137, September 2015. [ bib | DOI | http | .pdf | Abstract ]
[55] Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, and Stacey Son. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. Technical Report UCAM-CL-TR-876, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ]
[56] Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, and Jonathan Woodruff. Capability Hardware Enhanced RISC Instructions: CHERI Programmer's Guide. Technical Report UCAM-CL-TR-877, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ]
[57] Anthony C. J. Fox. Improved tool support for machine-code decompilation in HOL4. In ITP 2015:Interactive Theorem Proving - 6th International Conference, Nanjing, China, pages 187-202, August 2015. [ bib | DOI | http | .pdf | Abstract ]
[58] David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation. In USENIX Security 2015: 24th USENIX Security Symposium, Washington, D.C., USA, pages 223-238, August 2015. [ bib | http | .pdf | Abstract ]
[59] Ali Sezgin and Serdar Tasiran. Moving around: Lipton's reduction for TSO - (regular submission). In VSTTE 2015: Verified Software: Theories, Tools, and Experiments - 7th International Conference, San Francisco, CA, USA. Revised Selected Papers, pages 165-182, July 2015. [ bib | DOI | http | Abstract ]
[60] Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). In MFPS 2015: Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, pages 3-18, June 2015. [ bib | DOI | http | .pdf | Abstract ]
[61] S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell. Rigorous architectural modelling for production multiprocessors, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[62] Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In Security and Privacy 2015: Proceedings of the 36th IEEE Symposium on Security and Privacy (“Oakland”), May 2015. [ bib | DOI | .pdf | Abstract ]
[63] 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 ]
[64] David Kaloper Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[65] A. M. Pitts, J. Matthiesen, and J. Derikx. A dependent type theory with abstractable names. In I. Mackie and M. Ayala-Rincon, editors, LSFA 2014: Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications, volume 312 of Electronic Notes in Theoretical Computer Science, pages 19-50. Elsevier, April 2015. [ bib | DOI | http | Abstract ]
[66] 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 ]
[67] Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. A separation logic for fictional sequential consistency. In ESOP 2015, April 2015. [ bib | DOI | Abstract ]
[68] Azalea Raad, Jules Villard, and Philippa Gardner. CoLoSL: Concurrent local subjective logic. In ESOP 2015, April 2015. [ bib | DOI | .pdf | Abstract ]
[69] Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. Logical Methods in Computer Science, 11(1):1-33, April 2015. [ bib | DOI | http | Abstract ]
[70] Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In ASPLOS 2015: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, Istanbul, Turkey, pages 577-591, March 2015. [ bib | DOI | http | Abstract ]
[71] 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 ]
[72] David Kaloper Meršinjak and Hannes Mehnert. Trustworthy secure modular operating system engineering. Invited talk at 31st Chaos Communication Congress (31C3), January 2015. [ bib | Abstract ]
[73] 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 ]
[74] 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 ]
[75] Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. In ICFP 2014: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 175-188, New York, NY, USA, September 2014. ACM. [ bib | DOI | http | .pdf | Abstract ]
[76] Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. In Frédéric Lang and Francesco Flammini, editors, FMICS 2014: Formal Methods for Industrial Critical Systems, volume 8718 of Lecture Notes in Computer Science, pages 185-199. Springer, September 2014. [ bib | DOI | .pdf | Abstract ]
[77] Hannes Mehnert and David Kaloper Mersinjak. Transport Layer Security purely in OCaml. In Proceedings of the ACM OCaml 2014 Workshop, September 2014. [ bib | .pdf | Abstract ]
[78] Basile Clement. Running programming language specifications, August 2014. MPRI report. [ bib ]
[79] Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. TaDA: A logic for time and data abstraction. In Richard Jones, editor, ECOOP 2014, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer Berlin Heidelberg, July 2014. [ bib | DOI | http | Abstract ]
[80] Philippa Gardner, Azalea Raad, Mark J. Wheelhouse, and Adam Wright. Abstract local reasoning for concurrent libraries: Mind the gap. MFPS 2014: Electr. Notes Theor. Comput. Sci., 308:147-166, June 2014. [ bib | DOI | http | Abstract ]
[81] 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 ]
[82] Philippa Gardner, Gian Ntzik, and Adam Wright. Local reasoning for the POSIX file system. In ESOP 2014: Programming Languages and Systems - 23rd European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, pages 169-188, April 2014. [ bib | DOI | http | Abstract ]
[83] Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O'Hearn. Developments in concurrent Kleene algebra. In RAMiCS 2014: Relational and Algebraic Methods in Computer Science - 14th International Conference, Marienstatt, Germany, pages 1-18, April 2014. [ bib | DOI | http | Abstract ]
[84] Reinoud Elhorst. Lowering C11 atomics for ARM in LLVM, March 2014. [ bib | .pdf | Abstract ]
[85] 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 ]
[86] 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 ]
[87] 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.