I am a third year Ph.D. student working in the Theory and Semantics Group at the Computer Laboratory, University of Cambridge. My supervisors are Peter Sewell and Matthew Parkinson.
My interests are (not limited to): module systems, versioning, computer-aided verification, compiler optimisation, transactions.
I have completed the
Isabelle/HOL proof of LJ's progress and well-formedness preservation ---
see LJ's page for details.
| Project Name | A Short Description | Release Date |
|---|---|---|
| an extension of JAM that gives a more expressive & intuitive semantics | Aug. 2007 | |
| LJAM | a core design and semantic definition of the Java Module System | Mar. 2007 |
| LJ | a fully-formalized and extensible minimal imperative fragment of Java | Nov. 2006 |
| HashCaml | an OCaml extension with support for type-safe marshalling | Apr. 2006 |
Ott: Effective Tool Support for the Working Semanticist
[pdf]
[ps]
[bib]
[doi]
[www]
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine,
Thomas Ridge, Susmit Sarkar, and Rok Strniša.
© ACM, 2007. In ICFP
2007.
The Java Module System: Core Design and Semantic Definition
[pdf]
[ps]
[bib]
[doi]
[www]
Rok Strniša, Peter Sewell, and
Matthew Parkinson.
© ACM, 2007. In
ooPSLA 2007.
Type-Safe Distributed Programming for OCaml
[pdf]
[ps]
[bib]
[doi]
[www]
John
Billings, Peter Sewell, Mark Shinwell, and Rok Strniša.
© ACM, 2006. In 2006
ACM SIGPLAN Workshop on ML.
My supervision guidelines for supervisees.
| Address: | University of Cambridge Computer Laboratory William Gates Building 15 JJ Thomson Avenue Cambridge CB3 0FD, UK |
| Email: | Rok.Strnisa (at) cl.cam.ac.uk |
| Phone: | +44 (0) 1223 763594 |
| Office: | FE22 |
|
|