papers.bib

@inproceedings{ccasin:popl14,
  author = {Chris Casinghino and Vilhelm Sj\"{o}berg and Stephanie Weirich},
  title = {Combining Proofs and Programs in a Dependently Typed Langauge},
  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}
}