Steffen Smolka
Office: 442 Gates Hall
Email: [lastname]@cs.cornell.edu
Google Scholar
Github
PhD Student
Department of Computer Science
Cornell University
Adviser: Nate Foster
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 5minute talk on A DomainTheoretic 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 SoftwareDefined 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)
Publications
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
[ conference version  full paper  slides ] 
POPL 17 
A Fast Compiler for NetKAT
[ paper  slides  video  code  award ]

ICFP 15 
Semiintelligible Isar Proofs from MachineGenerated Proofs
[ paper ]

JAR 15 
Robust, SemiIntelligible Isabelle Proofs from ATP Proofs
[ paper  slides ]

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