| {CertiKOS}: An extensible architecture for building certified concurrent {OS} kernels R Gu, Z Shao, H Chen, XN Wu, J Kim, V Sjöberg, D Costanzo 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2016 | 323 | 2016 |
| Software foundations BC Pierce, C Casinghino, M Gaboardi, M Greenberg, C Hriţcu, V Sjöberg, ... Webpage: http://www. cis. upenn. edu/bcpierce/sf/current/index. html, 16, 2010 | 208 | 2010 |
| Reactive noninterference A Bohannon, BC Pierce, V Sjöberg, S Weirich, S Zdancewic Proceedings of the 16th ACM conference on Computer and communications …, 2009 | 128 | 2009 |
| Combining proofs and programs in a dependently typed language C Casinghino, V Sjöberg, S Weirich ACM SIGPLAN Notices 49 (1), 33-45, 2014 | 87 | 2014 |
| Programming language foundations BC Pierce, AA de Amorim, C Casinghino, M Gaboardi, M Greenberg, ... Software Foundations series 2, 2018 | 54 | 2018 |
| Certified concurrent abstraction layers R Gu, Z Shao, J Kim, X Wu, J Koenig, V Sjöberg, H Chen, D Costanzo, ... ACM SIGPLAN Notices 53 (4), 646-661, 2018 | 51 | 2018 |
| Logical foundations BC Pierce, AA de Amorim, C Casinghino, M Gaboardi, M Greenberg, ... Software Foundations series 1, 2018 | 44 | 2018 |
| Building certified concurrent OS kernels R Gu, Z Shao, H Chen, J Kim, J Koenig, X Wu, V Sjöberg, D Costanzo Communications of the ACM 62 (10), 89-99, 2019 | 38 | 2019 |
| Irrelevance, heterogeneous equality, and call-by-value dependent type systems V Sjöberg, C Casinghino, KY Ahn, N Collins, HD Eades III, P Fu, ... arXiv preprint arXiv:1202.2923, 2012 | 35 | 2012 |
| Safety and liveness of MCS lock—layer by layer J Kim, V Sjöberg, R Gu, Z Shao Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou …, 2017 | 34 | 2017 |
| Programming up to congruence V Sjöberg, S Weirich Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2015 | 34 | 2015 |
| Equational reasoning about programs with general recursion and call-by-value semantics G Kimmell, A Stump, HD Eades III, P Fu, T Sheard, S Weirich, ... Proceedings of the sixth workshop on Programming languages meets program …, 2012 | 34 | 2012 |
| Dependent interoperability PM Osera, V Sjöberg, S Zdancewic Proceedings of the sixth workshop on Programming languages meets program …, 2012 | 31 | 2012 |
| Dependent types and program equivalence L Jia, J Zhao, V Sjöberg, S Weirich Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010 | 24 | 2010 |
| Software foundations. 2010 B Pierce, C Casinghino, M Greenberg, V Sjöberg, B Yorgey URL https://softwarefoundations. cis. upenn. edu, 2010 | 22 | 2010 |
| Software Foundations. Electronic textbook, 2012 BC Pierce, C Casinghino, M Gaboardi, M Greenberg, C Hritcu, V Sjöberg, ... | 18 | |
| Step-indexed normalization for a language with general recursion C Casinghino, V Sjöberg, S Weirich arXiv preprint arXiv:1202.2918, 2012 | 16 | 2012 |
| A dependently typed language with nontermination V Sjoberg University of Pennsylvania, 2015 | 14 | 2015 |
| Logical Foundations. Software Foundations series, volume 1. Electronic textbook, May 2018. Version 5.5 BC Pierce, AA de Amorim, C Casinghino, M Gaboardi, M Greenberg, ... | 14 | |
| Software Foundations. Electronic textbook, 2016. Version 4.0 BC Pierce, AA de Amorim, C Casinghino, M Gaboardi, M Greenberg, ... | 12 | |
