Research Overview

I enjoy working on problems at the intersection of theory and practice. My interests include language design, (probabilisitc) semantics, compilers, automata theory, formal verification, and algorithms.

I am passionately working on making networks more programmable.

Before coming to Cornell, I received a B.Sc. in Computer Science from Technische Universität München, where I worked with Jasmin Blanchette on the interactive theorem prover Isabelle.

Recent News & Talks

Mar 17 I'm excited to attend the Bellairs workshop on Probabilistic Programming Languages in Barbados.
Jan 17 The slides for our POPL'17 paper Cantor Meets Scott are now online. (A recording will follow soon.)
Oct 16 Cantor meets Scott at POPL 2017 in Paris. See you there!
Oct 16 Our paper A Fast Compiler for NetKAT was recognized as a SIGPLAN Research Highlight!
Sep 16 I am visiting Stanford until February. I am also working part time at Barefoot Networks.
Jul 16 I gave a 5-minute talk on A Domain-Theoretic Foundation for Probabilistic NetKAT at Lake Placid.
June 16 I serve on the Artifact Evaluation Committee for POPL 2017.
June 16 I gave a talk on efficent language abstractions for SDN at the Network Programming Retreat in NYC.
May 16 I discussed current work on probabilistic NetKAT at NEPLS.
Mar 16 I'm attending the Bellairs Workshop on Formal Methods for Software-Defined Networks in Barbados.
June 15 I am excited to work with with Dimitrios Vytiniotis at Microsoft Research in Cambridge over the summer.

Projects (current & past)


Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
conference version | full paper | slides ]
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva.
A Fast Compiler for NetKAT paper | slides | video | code | award ]
Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha
Semi-intelligible Isar Proofs from Machine-Generated Proofs paper ]
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Smolka, and Albert Steckermeier
JAR 15
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs paper | slides ]
Steffen Smolka and Jasmin Christian Blanchette
PxTP 13


CS 4120/5120: Compilers, Cornell University, Spring 2016
Introduction to Computer Science 2, Technische Universität München, Fall 2011