Steven S. Lyubomirsky

sslyu (at)

I am a third-year Ph.D. student at the University of Washington's Programming Languages and Software Engineering group. My adviser is Zachary Tatlock. I am broadly interested in compilers and tools related to compilers, namely in producing tools to enable new kinds of programming, such tools built on proof assistants and SMT solvers to develop programs with proven correctness properties and compilers for domain-specific languages that better encode expert knowledge to achieve greater performance and expressiveness than general-purpose languages and libraries.

Presently I am part of SAMPL, which is an interdisciplinary research group holistically exploring problems spanning the machine learning stack. I am specifically working on the Relay project, whose purpose is to enable new abstractions and optimizations in machine-learning frameworks by providing an expressive intermediate representation and new compilation pipeline for TVM.

I have previously worked on the Bagpipe project, for verifying BGP configurations. An offshoot of the Bagpipe project is the SpaceSearch library, allowing for reasoning about the reduction of a problem to SMT in Coq and then extracting the proof of correctness to a solver-aided tool in Rosette.


Conference Papers

Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. 2017. SpaceSearch: a library for building and verifying solver-aided tools. Proc. ACM Program. Lang. 1, ICFP, Article 25 (August 2017), 28 pages. DOI:

Workshop Papers

Jared Roesch, Steven Lyubomirsky, Logan Weber, Josh Pollock, Marisa Kirisame, Tianqi Chen, and Zachary Tatlock. 2018. Relay: a new IR for machine learning frameworks. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL 2018). ACM, New York, NY, USA, 58-68. DOI:

Note: My website's background is a late Victorian pattern from William Morris and Co.