Publications

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

Recent papers

  • The ImpFS filesystem
    Tom Ridge.
    ICFP 2020, OCaml'20 workshop.
    ifcp20 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.
    IFCP 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.