Stephanie Weirich's Publications
Copyright Information
Works in Progress
[1] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence. Submitted for publication, July 2014. [ PDF ]
[2] Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee. Verified Generation of Glue Code for ROS-based Control Systems. Submitted for publication., 2014.

Conferences and Workshops
[1] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe Zero-Cost Coercions for Haskell. In The 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, September 2014. To appear. [ PDF ]
[2] Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. Closed type families with overlapping equations. In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 671-683, San Diego, CA, USA, January 2014. [ PDF ]
[3] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining Proofs and Programs in a Dependently Typed Language. In POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 33-45, San Diego, CA, USA, 2014. [ PDF ]
[4] Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System FC with explicit kind equality. In Proceedings of The 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13, pages 275-286, Boston, MA, September 2013. [ PDF ]
[5] Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, and Insup Lee. Towards synthesis of platform-aware attack-resilient control systems: extended abstract. In HiCoNS '13: Proceedings of the 2nd ACM international conference on High confidence networked systems, pages 75-76, New York, NY, USA, 2013. [ DOI ]
[6] Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell Symposium, pages 117-130, Copenhagen, Denmark, September 2012. [ PDF ]
[7] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Step-Indexed Normalization for a Language with General Recursion. In Fourth workshop on Mathematically Structured Functional Programming (MSFP '12), pages 25-39, 2012. [ PDF ]
[8] 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, Heterogenous Equality, and Call-by-value Dependent Type Systems. In Fourth workshop on Mathematically Structured Functional Programming (MSFP '12), pages 112-162, 2012. [ PDF ]
[9] 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 Sixth ACM SIGPLAN Workshop Programming Languages meets Program Verification (PLPV '12), pages 15-26, 2012. [ PDF ]
[10] Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhaes. Giving Haskell A Promotion. In Seventh ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '12), pages 53-66, 2012. [ PDF ]
[11] Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 333-345, New York, NY, USA, 2011. [ PDF  http ]
[12] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level Computation. In POPL 11: 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, January 26-28, 2011. Austin, TX, USA., pages 227-240, January 2011. [ PDF  Abstract ]
[13] Tim Sheard, Aaron Stump, and Stephanie Weirich. Language-Based Verification Will Change The World. In 2010 FSE/SDP Workshop on the Future of Software Engineering Research, pages 343-348, November 2010. Position paper. [ PDF ]
[14] Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. Termination Casts: A Flexible Approach to Termination with General Recursion. In Workshop on Partiality and Recursion in Interactive Theorem Provers, pages 76-93, Edinburgh, Scotland, July 2010. [ PDF  Abstract ]
[15] Michael Greenberg, Benjamin Pierce, and Stephanie Weirich. Contracts Made Manifest. In 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 353-364, Madrid, Spain, January 2010. [ PDF  Abstract ]
[16] Limin Jia, Jianzhou Zhao, Vilhem Sjöberg, and Stephanie Weirich. Dependent types and Program Equivalence. In 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 275-286, Madrid, Spain, January 2010. [ PDF  Abstract ]
[17] Stephanie Weirich and Chris Casinghino. Arity-generic type-generic programming. In ACM SIGPLAN Workshop on Programming Languages Meets Program Verification (PLPV), pages 15-26, January 2010. [ PDF ]
[18] Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive Noninterference. In 16th ACM Conference on Computer and Communications Security, pages 79-90, November 2009. [ PDF  Abstract ]
[19] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. FPH: First-class polymorphism for Haskell. In ICFP 2008: The 13th ACM SIGPLAN International Conference on Functional Programming, pages 295-306, Victoria, BC, Canada, September 2008. [ Project  PDF  Abstract ]
[20] Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 3-15, January 2008. [ Project  PDF  Abstract ]
[21] Dimitrios Vytiniotis and Stephanie Weirich. Dependent types: Easy as PIE. In Marco T. Morazán and Henrik Nilsson, editors, Draft Proceedings of the 8th Symposium on Trends in Functional Programming, pages XVII-1-XVII-15. Dept. of Math and Computer Science, Seton Hall University, April 2007. TR-SHU-CS-2007-04-1. [ PDF ]
[22] Dimitrios Vytiniotis and Stephanie Weirich. Free theorems and runtime type representations. In Mathematical Foundations of Programming Semantics (MFPS XXIII), pages 357-373, New Orleans, LA, USA, April 2007. [ Project  PDF  PS  Abstract ]
[23] Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1-12, Portland, OR, USA, September 2006. [ Project  PDF  Abstract ]
[24] Geoffrey Washburn and Stephanie Weirich. Good Advice for Type-directed Programming: Aspect-oriented Programming and Extensible Generic Functions. In Workshop on Generic Programming (WGP), pages 33-44, Portland, OR, USA, September 2006. [ Project  PDF  Abstract ]
[25] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Boxy type inference for higher-rank types and impredicativity. In International Conference on Functional Programming (ICFP), pages 251-262, Portland, OR, USA, September 2006. [ Project  PDF  Abstract ]
[26] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In International Conference on Functional Programming (ICFP), pages 50-61, Portland, OR, USA, September 2006. [ Project  PDF  Abstract ]
[27] Brian Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal Reasoning Techniques in Coq. In International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP), pages 60-69, Seattle, WA, USA, August 2006. [ Project  PDF  Abstract ]
[28] Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, and Steve Zdancewic. It is Time to Mechanize Programming Language Metatheory. In Verified Software: Theories, Tools, Experiments (VS:TTE), pages 26-30, Zürich, Switzerland, October 2005. [ Project  PDF  Abstract ]
[29] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. PolyAML: A polymorphic aspect-oriented functional programmming language. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 306-319, Tallinn, Estonia, September 2005. [ Project  PDF  PS  Abstract ]
[30] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized Metatheory for the Masses: The POPLmark Challenge. In The 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 50-65, Oxford, UK, August 2005. [ Project  PDF  PS  Abstract ]
[31] Geoffrey Washburn and Stephanie Weirich. Generalizing Parametricity Using Information Flow. In Twentieth Annual IEEE Symposium on. Logic in Computer Science (LICS 2005), pages 62-71, Chicago, IL, USA, June 2005. [ Project  PDF  PS  Abstract ]
[32] Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An Open and Shut Typecase. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 13-24, Long Beach, CA, USA, January 2005. [ PS  Abstract ]
[33] Stephanie Weirich and Liang Huang. A Design for Type-Directed Java. In Viviana Bono, editor, Workshop on Object-Oriented Developments (WOOD), ENTCS, pages 117-136, August 2004. [ Project  PDF  PS  Abstract ]
[34] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism. In ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 249-262, Uppsala, Sweden, August 2003. [ PDF  PS  Abstract ]
[35] Stephanie Weirich. Higher-Order Intensional Type Analysis. In Daniel Le Métayer, editor, 11th European Symposium on Programming (ESOP), pages 98-114, Grenoble, France, April 2002. [ PDF  PS  Abstract ]
[36] Stephanie Weirich. Encoding Intensional Type Analysis. In D. Sands, editor, 10th European Symposium on Programming (ESOP), pages 92-106, Genova, Italy, April 2001. [ PDF  PS  http  Abstract ]
[37] Stephanie Weirich. Type-Safe Cast: Functional Pearl. In Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 58-67, Montreal, Canada, September 2000. [ PDF  PS  Abstract ]
[38] Karl Crary and Stephanie Weirich. Resource Bound Certification. In The Twenty-Seventh ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 184-198, Boston, MA, USA, January 2000. [ PDF  PS  Abstract ]
[39] Karl Crary and Stephanie Weirich. Flexible Type Analysis. In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 233-248, Paris, France, September 1999. [ PDF  PS  Abstract ]
[40] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed Assembly Language. In Second ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35, Atlanta, GA, USA, May 1999. Published as INRIA research report number 0228, March 1999. [ PDF  PS  Abstract ]
[41] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type Erasure Semantics. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 301-313, Baltimore, MD, USA, September 1998. [ PDF  PS  Abstract ]
[42] Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching Bugs in the Web of Program Invariants. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 23-32, 1996. [ PDF  PS  Abstract ]

Journal Articles
[1] Garrin Kimmel, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathin Collins, and Ki Yunh Anh. Equational reasoning about programs with general recursion and call-by-value semantics. Progress in Informatics, (10):19-48, March 2013. [ http ]
[2] Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. Journal of Functional Programming, 22(3):225-274, May 2012.
[3] Dimitrios Vytiniotis and Stephanie Weirich. Parametricity, Type Equality and Higher-order Polymorphism. Journal of Functional Programming, 20(2):175-210, March 2010. [ PDF  Abstract ]
[4] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. AspectML: A Polymorphic Aspect-oriented Functional Programming Language. ACM Transactions on Programming Languages, 30(3):1-60, May 2008. [ DOI  Project  PDF  Abstract ]
[5] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism. Journal of Functional Programming, 18(1):87-140, January 2008. [ PDF  Abstract ]
[6] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Journal of Functional Programming, 17(1):1-82, January 2007. [ Project  PDF  Abstract ]
[7] Stephanie Weirich. Type-Safe Run-time Polytypic Programming. Journal of Functional Programming, 16(10):681-710, November 2006. [ PDF  Abstract ]
[8] Stephanie Weirich. Type-Safe Cast. Journal of Functional Programming, 14(6):681-695, November 2004. [ PDF  Abstract ]
[9] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type Erasure Semantics. Journal of Functional Programming, 12(6):567-600, November 2002. [ PDF  Abstract ]

Book Chapters
[1] Stephanie Weirich. Type Systems. In Teofilo F. Gonzalez, Jorge Diaz-Herrera, and Allen Tucker, editors, Computing Handbook, 3rd ed. (1), pages 70:1-39. CRC Press, 2014.
[2] Stephanie Weirich and Chris Casinghino. Generic Programming with Dependent Types. In Jeremy Gibbons, editor, Generic and Indexed Programming, number 7470 in Lecture Notes in Computer Science, pages 217-258. Springer-Verlag Berlin Heidelberg, 2012. [ PDF ]
[3] Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and Flexible Dynamic Linking of Native Code. In R. Harper, editor, Types in Compilation: Third International Workshop, TIC 2000; Montreal, Canada, September 21, 2000; Revised Selected Papers, volume 2071 of Lecture Notes in Computer Science, pages 147-176. Springer, 2001. [ PDF  PS  http  Abstract ]

Thesis
[1] Stephanie Weirich. Programming With Types. PhD thesis, Cornell University, August 2002. [ PDF  PS  Abstract ]

Technical Reports
[1] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence (Extended Version). Technical report, July 2014. [ PDF ]
[2] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe Zero-cost Coercions for Haskell (Extended Version). Technical Report MS-CIS-14-07, Univ. of Pennsylvania, April 2014. [ PDF ]
[3] Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining Proofs and Programs in a Dependently Typed Language (With Technical Appendix). Technical Report MS-CIS-13-08, University of Pennsylvania, November 2013. [ PDF ]
[4] Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. Closed type families with overlapping equations (Extended version). Technical Report MS-CIS-13-10, University of Pennsylvania, November 2013. [ PDF ]
[5] Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. Generative Type Abstraction and Type-level Computation (Extended Version). Technical report, November 2010. [ PDF  Abstract ]
[6] Brian Aydemir and Stephanie Weirich. LNgen: Tool Support for Locally Nameless Representations. Technical Report MS-CIS-10-24, Computer and Information Science, University of Pennsylvania, June 2010. [ Project  PDF ]
[7] Aaron Stump, Vilhelm Sjöberg, and Stephanie Weirich. Termination Casts: A Flexible Approach to Termination with General Recursion (Technical Appendix). Technical Report MS-CIS-10-21, University of Pennsylvania Department of Computer and Information Science, 2010. [ PDF ]
[8] Brian Aydemir, Steve Zdancewic, and Stephanie Weirich. Abstracting Syntax. Technical Report MS-CIS-09-06, Computer and Information Science, University of Pennsylvania, March 2009. [ Project  PDF ]
[9] Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. Manifest Security. Technical report, January 2007. White paper. [ PDF ]
[10] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Boxy type inference for higher-rank types and impredicativity, Technical Appendix. Technical Report MS-CIS-05-23, University of Pennsylvania, April 2006. [ Project  PDF ]
[11] Dimitrios Vytiniotis, Stephanie Weirich, and Simon L. Peyton Jones. Simple unification-based type inference for GADTs, Technical Appendix. Technical Report MS-CIS-05-22, University of Pennsylvania, April 2006. [ Project  PDF ]
[12] Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types (Technical appendix). Technical Report MIS-CIS-05-14, University of Pennsylvania, July 2005. [ Project  PDF ]
[13] Geoffrey Washburn and Stephanie Weirich. Generalizing Parametricity Using Information Flow (Extended version). Technical Report MS-CIS-05-04, Computer and Information Science, University of Pennsylvania, July 2005. [ PDF  Abstract ]
[14] Daniel S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. PolyAML: A Polymorphic Aspect-Oriented Functional Programming Language (Extended Version). Technical Report MS-CIS-05-07, University of Pennsylvania, Department of Computer and Information Science, 2005. [ PDF  Abstract ]
[15] Dan S. Dantas, David Walker, Geoffrey Washburn, and Stephanie Weirich. Analyzing Polymorphic Advice. Technical Report TR-717-04, Princeton University Computer Science, December 2004. [ Project  PDF  Abstract ]
[16] Liang Huang and Stephanie Weirich. A Design for Type-Directed Programming in Java (Extended Version). Technical Report MS-CIS-04-11, University of Pennsylvania, Computer and Information Science, October 2004. [ PDF  PS ]
[17] Dimtrios Vytiniotis, Geoffrey Washburn, and Stephanie Weirich. An Open and Shut Typecase (Extended Version). Technical Report MS-CIS-04-26, University of Pennsylvania, Computer and Information Science, October 2004. [ PDF  PS  Abstract ]
[18] Simon L. Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: Practical Type Inference for Generalised Algebraic Dataypes. Technical Report MS-CIS-05-26, University of Pennsylvania, Computer and Information Science Department, Levine Hall, 3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389, July 2004. [ Project  PDF  Abstract ]
[19] Geoffrey Washburn and Stephanie Weirich. Boxes Go Bananas: Encoding Higher-order Abstract Syntax with Parametric Polymorphism (Extended version). Technical Report MS-CIS-03-26, University of Pennsylvania, Computer and Information Science, September 2003. [ PDF  PS  Abstract ]
[20] Michael Hicks and Stephanie Weirich. A Calculus for Dynamic Loading. Technical Report MS-CIS-00-07, University of Pennsylvania, April 2000. [ PDF  Abstract ]
[21] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional Polymorphism in Type Erasure Semantics (Extended Version). Technical Report TR98-1721, Cornell University, Computer Science, November 1998. [ PDF  PS ]

Copyright Information
The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Parts of this page were generated by bibtex2html Last modified: Wed Sep 3 11:09:10 CEST 2014