|
[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 |
.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 ]
|