I've moved to UPenn, and this page is no longer being updated. Visit my new page.
Most recently at Cambridge I was a Research Associate on the Network-as-a-Service project, and belonged to the Networks and Operating Systems group. Previously I wrote a PhD dissertation on proof
translation in the Automated Reasoning
group, supervised by Larry
Paulson. I was very fortunate to have a long collaboration with Christoph Benzmueller. I
also gained a lot from interning at MSR multiple
times, where I worked on the application of logic to security and biological
Before that I worked in the Schwichtenberg group after writing an MSc dissertation on the validation of refactorings. Prior to that I participated in the Vulcanus in Japan programme, after finishing my first degree in Malta.
Writing software is one of the best things about computer science. Here I link to bits of software I've written or contributed to. Other small things can be found on my Github page.
Most of the work I've done so for is related to logic. This also applies to the software I've written or contributed to.
Recently I've been working more on networking and systems.
I enjoy teaching, especially in the the small-group tutorial style done in Cambridge (called "supervisions"). I've supervised the following courses:
- Compiler construction
- Computer networking
- Concepts in programming languages
- Denotational semantics
- Discrete maths
- Foundations of computer science
- Logic and proof
- Operational semantics
- Optimising compilers
- Software and interface design
- Specification and verification
- Unix tools
I've been a frequent user of functional languages for several years.
Some years ago I wrote up some tips on Haskell programming to help spread the functional word.
Another great thing about computer science is that programs aren't the only objects you can construct -- you can also construct proofs using a similar mindset and tools as you would construct programs.
Proofs are used to communicate rigorous and formal arguments justifying an assertion. Often this assertion is something like "for any input, this program's behaviour agrees with its specification".
- Kneecap: model-based generation of network traffic. 2016
N.S., Richard Mortier
Satisfiability Modulo Theories workshop. (Accepted)
- Light at the middle of the tunnel: middleboxes for selective
disclosure of network monitoring to distrusted parties. 2016
N.S., Markulf Kohlweiss, Andrew W. Moore
HotMiddlebox. (In press)
- FLICK: Developing and Running Application-Specific Network Services. 2016
Abdul Alim, Richard G. Clegg, Luo Mai, Lukas Rupprecht, Eric Seckler, Paolo
Costa, Peter Pietzuch, Alexander L. Wolf, N.S., Jon Crowcroft, Anil Madhavapeddy, Andrew W. Moore, Richard Mortier,
Masoud Koleini, Luis Oviedo, Derek McAuley, Matteo Migliavacca
USENIX Annual Technical Conference. (In press)
- Proofs and reconstructions. 2015
N.S., Christoph Benzmueller, Lawrence C. Paulson
Frontiers of Combining Systems. (In press)
- Selective Disclosure in Datalog-Based Trust Management. 2013
N.S., Moritz Y. Becker, Markulf Kohlweiss
Security and Trust Management. Volume 8203 of the series Lecture Notes in Computer Science. pp 160-175
- LEO-II and Satallax on the Sledgehammer test bench. 2013
N.S., Jasmin C. Blanchette, Lawrence C. Paulson
Journal of Applied Logic. Volume 11, Issue 1. pp 91–102.
- Foundations of Logic-Based Trust Management. 2012
Moritz Y. Becker, Alessandra Russo, N.S.
IEEE Symposium on Security and Privacy. pp 161-175.
- Mechanical verification of refactorings. 2008.
N.S., Simon Thompson
Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Program Manipulation. pp 51-60.
I also enjoy writing non-technical articles about scientific ideas or their application.