Vilhelm Sjöberg

I am a Research Scientist at CertiK, where I work on applying formal verification to smart contracts. I also have an (unpaid) affiliate position at Yale University and collaborate with researchers at Yale.

In 2015-2018 I was a postdoc and associate research scientist in the FLINT group at the Department of Computer Science, Yale University, working with Zhong Shao on verified systems software. Before that, I did my phd at the University of Pennsylvania. My advisor was Stephanie Weirich.

My research interests are in software verification, programming languages, type systems and logic.

Contact Information

Email:   vilhelm.sjoberg@yale.edu
Office:   313

Publications

[1]	Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan Newman Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 2018. [ bib ]
[2]	Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, and Zhong Shao. Safety and liveness of mcs lock-layer by layer. In APLAS 2017: 15th Asian Symposium on Programming Languages and Systems, 2017. [ bib | techreport version ]
[3]	Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, and Vilhelm Sjöberg. Certikos: An extensible architecture for building certified concurrent OS kernels. In OSDI '16: 12th USENIX Symposium on Operating Systems Design and Implementation, 2016. [ bib | .pdf ]
[4]	Vilhem Sjöberg. A Dependently Typed Language with Nontermination. PhD thesis, University of Pennsylvania, 2015. [ bib | Coq proofs | .pdf ]
[5]	Vilhem Sjöberg and Stephanie Weirich. Programming up to congruence. In POPL '15: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015. [ bib | techreport version | .pdf ]
[6]	Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs in a dependently typed language. In POPL '14: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014. [ bib | techreport version | .pdf ]
[7]	Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In James Chapman and Paul Blain Levy, editors, MSFP '12: Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming. Open Publishing Association, 2012. [ bib | .pdf ]
[8]	Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Step-indexed normalization for a language with general recursion. In James Chapman and Paul Blain Levy, editors, MSFP '12: Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming. Open Publishing Association, 2012. [ bib | .pdf ]
[9]	Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn. Equational reasoning about programs with general recursion and call-by-value semantics. In PLPV '12: Proceedings of the sixth workshop on Programming languages meets program verification, 2012. [ bib | .pdf ]
[10]	Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent interoperability. In PLPV '12: Proceedings of the sixth workshop on Programming languages meets program verification, 2012. [ bib | techreport version | .pdf ]
[11]	Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Distributed electronically, 2011. [ bib | http ]
[12]	Vilhelm Sjöberg and Aaron Stump. Equality, quasi-implicit products, and large eliminations. In ITRS '10: Proceedings of the Fifth Workshop on Intersection Types and Related Systems, 2010. [ bib | techreport version | .pdf ]
[13]	Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. Termination casts: A flexible approach to termination with general recursion. In PAR '10: Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010. [ bib | techreport version | .pdf ]
[14]	Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, and Stephanie Weirich. Dependent types and program equivalence. In POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2010. [ bib | .pdf ]
[15]	Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive noninterference. In CCS '09: Proceedings of the 16th ACM conference on Computer and communications security, New York, NY, USA, 2009. ACM. [ bib ]