[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 SIGPLANSIGACT Symposium on Principles of
Programming Languages, 2015.
[ bib 
.pdf ]

[3]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining proofs and programs in a dependently typed language.
In POPL '14: 41st ACM SIGPLANSIGACT 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 callbyvalue 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.
Stepindexed 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
callbyvalue semantics.
In PLPV '12: Proceedings of the sixth workshop on Programming
languages meets program verification, 2012.
[ bib 
.pdf ]

[7]

PeterMichael 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, quasiimplicit 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 SIGPLANSIGACT
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 ]
