papers.bib
@phdthesis{sjoberg:thesis,
author = {Vilhem Sj\"oberg},
title = {A Dependently Typed Language with Nontermination},
year = {2015},
school = {University of Pennsylvania},
pdf = {papers/thesis.pdf},
coq = {papers/step_teqt.tar.gz}
}
@inproceedings{gu:pldi18,
title = {Certified concurrent abstraction layers},
author = {Gu, Ronghui and Shao, Zhong and Kim, Jieung and Wu, Xiongnan Newman and Koenig, J{\'e}r{\'e}mie and Sj{\"o}berg, Vilhelm and Chen, Hao and Costanzo, David and Ramananandro, Tahina},
booktitle = {Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {646--661},
year = {2018},
organization = {ACM}
}
@inproceedings{kim:aplas17,
author = {Jieung Kim and Vilhelm Sj\"oberg and Ronghui Gu and Zhong Shao},
title = {Safety and Liveness of MCS Lock---Layer by Layer},
year = 2017,
booktitle = {APLAS 2017: 15th Asian Symposium on Programming Languages and Systems},
techreport = {flint.cs.yale.edu/flint/publications/mcslock-tr.pdf}
}
@inproceedings{gu:osdi16,
author = {Ronghui Gu and Zhong Shao and Hao Chen and Xiongnan (Newman) Wu and Jieung Kim and Vilhelm Sj\"oberg},
title = {CertiKOS: An Extensible Architecture for Building Certified Concurrent {OS} Kernels},
year = 2016,
booktitle = {OSDI '16: 12th USENIX Symposium on Operating Systems Design and
Implementation},
pdf = {papers/osdi16certikos.pdf}
}
@inproceedings{sjoberg:popl15,
author = {Vilhem Sj\"oberg and Stephanie Weirich},
title = {Programming up to Congruence},
booktitle = {POPL '15: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = 2015,
doi = {10.1145/2676726.2676974},
pdf = {papers/popl15congruence.pdf},
techreport = {http://repository.upenn.edu/cis_reports/992/}
}
@inproceedings{ccasin:popl14,
author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
title = {Combining Proofs and Programs in a Dependently Typed Language},
booktitle = {POPL '14: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = {2014},
doi = {10.1145/2535838.2535883},
pdf = {papers/popl14combining.pdf},
techreport = {http://repository.upenn.edu/cis_reports/985/}
}
@inproceedings{sjoberg:msfp12,
author = {Vilhelm Sj\"oberg and Chris Casinghino and Ki Yung Ahn and
Nathan Collins and Harley D. Eades III and Peng Fu
and Garrin Kimmell and Tim Sheard and Aaron Stump
and Stephanie Weirich},
title = {Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems},
booktitle = {MSFP '12: Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming},
year = 2012,
editor = {Chapman, James and Levy, Paul Blain},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {76},
publisher = {Open Publishing Association},
pages = {112-162},
doi = {10.4204/EPTCS.76.9},
pdf = {papers/msfp12prog.pdf}
}
@inproceedings{ccasin:msfp12,
author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
title = {Step-Indexed Normalization for a Language with General Recursion},
booktitle = {MSFP '12: Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming},
year = 2012,
editor = {Chapman, James and Levy, Paul Blain},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {76},
publisher = {Open Publishing Association},
pages = {25-39},
doi = {10.4204/EPTCS.76.4},
pdf = {papers/msfp12log.pdf}
}
@inproceedings{kimmel:plpv12,
author = {Garrin Kimmell and Aaron Stump and Harley D. Eades III and
Peng Fu and Tim Sheard and Stephanie Weirich and Chris Casinghino
and Vilhelm Sj\"oberg and Nathan Collins and Ki Yung Ahn},
title = {Equational Reasoning about Programs with General Recursion and Call-by-value Semantics},
booktitle = {PLPV '12: Proceedings of the sixth workshop on Programming languages meets program verification},
year = 2012,
pdf = {papers/plpv12genrec.pdf},
doi = {10.1145/2103776.2103780}
}
@inproceedings{osera:plpv12,
author = {Osera, Peter-Michael and Sj\"{o}berg, Vilhelm and Zdancewic, Steve},
title = {Dependent interoperability},
booktitle = {PLPV '12: Proceedings of the sixth workshop on Programming languages meets program verification},
year = {2012},
pdf = {papers/plpv12interop.pdf},
techreport = {http://repository.upenn.edu/cis_reports/969/},
doi = {10.1145/2103776.2103779}
}
@book{Pierce:SF,
author = {Benjamin C. Pierce and Chris Casinghino and
Michael Greenberg and Vilhelm Sj\"oberg and Brent Yorgey},
title = {Software Foundations},
year = {2011},
publisher = {Distributed electronically},
documenturl = {http://www.cis.upenn.edu/~bcpierce/sf}
}
@inproceedings{sjoberg:quasi,
author = {Sj\"{o}berg, Vilhelm and Stump, Aaron},
title = {Equality, Quasi-Implicit Products, and Large Eliminations},
booktitle = {ITRS '10: Proceedings of the Fifth Workshop on Intersection Types and Related Systems},
year = {2010},
pdf = {papers/itrs10equality.pdf},
techreport = {papers/itrs10equality-long.pdf},
doi = {10.4204/EPTCS.45.7}
}
@inproceedings{stump:terminationscasts,
author = {Aaron Stump and Vilhelm Sj\"oberg and Stephanie Weirich},
title = {Termination Casts: A Flexible Approach to Termination with General Recursion},
booktitle = {PAR '10: Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers},
year = {2010},
doi = {10.4204/EPTCS.43.6},
pdf = {papers/par10terminationcasts.pdf},
techreport = {http://repository.upenn.edu/cis_reports/930/}
}
@inproceedings{jia:lambdaeek,
author = {Jia, Limin and Zhao, Jianzhou and Sj\"{o}berg, Vilhelm and Weirich, Stephanie},
title = {Dependent types and program equivalence},
booktitle = {POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
year = {2010},
pages = {275--286},
location = {Madrid, Spain},
pdf = {papers/popl10equivalence.pdf},
doi = {10.1145/1706299.1706333}
}
@inproceedings{Bohannon:09,
author = {Bohannon, Aaron and Pierce, Benjamin C. and Sj\"{o}berg, Vilhelm and Weirich, Stephanie and Zdancewic, Steve},
title = {Reactive Noninterference},
booktitle = {CCS '09: Proceedings of the 16th ACM conference on Computer and communications security},
year = {2009},
isbn = {978-1-60558-894-0},
pages = {79--90},
location = {Chicago, Illinois, USA},
doi = {http://doi.acm.org/10.1145/1653662.1653673},
publisher = {ACM},
address = {New York, NY, USA}
}