Publications

Bibtex/citation information: me@DBLP and me@Google Scholar

Recent papers

  • The ImpFS filesystem
    Tom Ridge.
    ICFP 2020, OCaml'20 workshop.
    icfp20 page / conference talk / current state video (2020 Aug)

  • A Key-Value store for OCaml.
    Tom Ridge.
    ICFP 2019, ML'19 workshop.
    icfp19 page / pdf / blog

  • Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.
    Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough.
    J. ACM 66, 1, Article 1 (December 2018), 77 pages.
    DOI / pdf@ACM / pdf@Cambridge Open Access

  • Direct Interpretation of Functional Programs for Debugging.
    John Whitington and Tom Ridge.
    OCaml'17 post proceedings.
    EPTCS, 2019.
    pdf

  • Visualizing the Evaluation of Functional Programs for Debugging.
    John Whitington and Tom Ridge.
    SLATE'17
    pdf

  • A B-tree library for OCaml.
    Tom Ridge.
    OCaml'17 workshop talk.
    pdf

  • SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems
    Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy and Peter Sewell.
    SOSP'15.
    sosp15 / pdf@sosp15

  • Lem: reusable engineering of real-world semantics.
    Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell.
    ICFP 2014.
    pdf@cam / lem@github

  • Simple, efficient, sound and complete combinator parsing for all context-free grammars, using an oracle.
    Tom Ridge.
    SLE 2014.
    pdf / extended version / old slides

Older papers

  • The 1st Verified Software Competition: Extended Experience Report.
    Tom Ridge et al.
    Extended version of FM 2011 paper.
    pdf

  • Simple, functional, sound and complete parsing for all context-free grammars.
    Tom Ridge.
    CPP 2011.
    paper and supporting material

  • The 1st Verified Software Competition: Experience report.
    Tom Ridge et al.
    FM 2011.
    pdf
    🏆 Winner of the best paper prize for FM'11

  • Ott: Effective tool support for the working semanticist.
    Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa.
    Journal of Functional Programming, 20(1):70--122, January 2010.
    ridge10ott-jfp.pdf

  • Simple, functional, sound and complete parsing for all context-free grammars (unpublished draft).
    Tom Ridge.
    ridge10parsing.pdf

  • A rely-guarantee proof system for x86-TSO.
    Tom Ridge.
    VSTTE 2010.
    ridge10vstte.pdf

  • TCP, UDP, and Sockets: Volume 3: The Service-level Specification.
    Tom Ridge, Michael Norrish, and Peter Sewell.
    Technical Report UCAM-CL-TR-742, University of Cambridge, Computer Laboratory, February 2009.
    UCAM-CL-TR-742.pdf

  • Verifying distributed systems: the operational approach.
    Tom Ridge.
    POPL 2009.
    ridge09popl.pdf

  • The semantics of x86-CC multiprocessor machine code.
    Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave.
    POPL 2009.
    popl09.pdf

  • A rigorous approach to networking: TCP, from implementation to protocol to service.
    Tom Ridge, Michael Norrish, and Peter Sewell.
    FM 2008.
    ridge08stream-spec.pdf

  • Ott: effective tool support for the working semanticist.
    Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, and Rok Strnisa.
    ICFP 2007.
    ott.pdf
    🏆 ICFP 10 year most influential paper award in 2017

  • Operational reasoning for concurrent Caml programs and weak memory models.
    Tom Ridge.
    TPHOLs 2007.
    ridge07tphols.pdf

  • Rigorous protocol design in practice: An optical packet-switch MAC in HOL.
    Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, and Peter Sewell.
    ICNP 2006.
    ridge06icnp.pdf

  • Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL.
    Tom Ridge
    Unpublished draft, but cited by others so included here. http://arxiv.org/abs/cs/0607058

  • To arrive where we started: experience of mechanizing binding.
    Tom Ridge.
    Workshop on Mechanizing Metatheory 2007.
    ridge07wmm.pdf

  • A mechanically verified, sound and complete theorem prover for FOL.
    Tom Ridge and James Margetson.
    TPHOLs 2005.
    prover.pdf

  • A long time ago I also made a few contributions to the Archive of Formal Proofs, including a version of Ramsey's theorem (infinitary version). Just follow the link and grep for Ridge.