Vilhelm Sjöberg
I am a postdoc in the FLINT group at the Department of Computer Science, Yale University. I work 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. In particular I like dependent types, which combine all of these.
Contact Information
Email: vilhelm.sjoberg@yale.edu
Office: 313
Publications
[1] | Vilhem Sjöberg. A Dependently Typed Language with Nontermination. PhD thesis, University of Pennsylvania, 2015. [ bib | Coq proofs | .pdf ] |
[2] | 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 | errata | techreport version | .pdf ] |
[3] | 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 ] |
[4] | 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 ] |
[5] | 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 ] |
[6] | 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 ] |
[7] | 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 ] |
[8] | Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Distributed electronically, 2011. [ bib | http ] |
[9] | 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 ] |
[10] | 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 ] |
[11] | 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 ] |
[12] | 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 ] |