Stephanie Weirich's Publications
Copyright Information
Works in Progress

Refereed Journal, Conference and Workshop Publications
[1] Yao Li and Stephanie Weirich. Program Adverbs and Tlön Embeddings. Proc. ACM Program. Lang., 6(ICFP), September 2022. Distinguished Paper Award. Artifact available. [ DOI  .pdf ]
[2] Pritam Choudhury, Harley Eades III, and Stephanie Weirich. A Dependent Dependency Calculus. In Ilya Sergey, editor, Programming Languages and Systems, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 403--430, Cham, 2022. Springer International Publishing. Artifact available. [ DOI  http  Abstract ]
[3] Yao Li, Li yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths. Proc. ACM Program. Lang., 5(ICFP), August 2021. [ DOI ]
[4] Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee. An Existential Crisis Resolved: Type inference for first-class existential types. Proc. ACM Program. Lang., 5(ICFP), August 2021. Distinguished Paper Award. [ DOI  .pdf ]
[5] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, and Stephanie Weirich. Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell Code. Journal of Functional Programming, 31:1--40, February 2021. [ DOI  .pdf ]
[6] Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie Weirich. A Graded Dependent Type System with a Usage-Aware Semantics. Proc. ACM Program. Lang., 5(POPL), January 2021. Artifact available. [ DOI  http ]
[7] Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-equivalence in Core Dependent Haskell. In Marc Bezem and Assia Mahboubi, editors, Post-proceedings of the 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics, pages 7:1--7:32, Dagstuhl, Germany, September 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [ DOI  http ]
[8] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg. A Role for Dependent Types in Haskell. Proc. ACM Program. Lang., 3(ICFP), 2019. [ DOI  .pdf ]
[9] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. Ready, Set, Verify! Applying Hs-to-coq to Real-world Haskell Code (Experience Report). Proc. ACM Program. Lang., 2(ICFP):89:1--89:16, July 2018. Artifact Available. [ DOI  http ]
[10] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and Stephanie Weirich. Total Haskell is Reasonable Coq. In Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'18). ACM, 2018. New York, NY, USA. [ DOI  PDF ]
[11] Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg. A Specification for Dependent Types in Haskell. Proc. ACM Program. Lang., 1(ICFP):31:1--31:29, August 2017. Artifact evaluated as "Available" and Reusable". [ DOI  http ]
[12] Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. [ DOI  arXiv  http  Abstract ]
[13] Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible Type Application. In European Symposium on Programming (ESOP), pages 229--254, April 2016. [ DOI  PDF ]
[14] Steven Keuchel, Stephanie Weirich, and Thomas Tom Schrijvers. Needle and Knot: Binder Boilerplate Tied Up. In European Symposium on Programming (ESOP), pages 419--445, April 2016. [ DOI ]
[15] Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Safe zero-cost coercions for Haskell. Journal of Functional Programming, 26, 2016. [ DOI  PDF  http  Abstract ]
[16] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence. In POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 369--382, Mumbai, India, January 2015. Artifact Evaluated. [ DOI  PDF ]
[17] Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, and Insup Lee. Verified ROS-Based Deployment of Platform-Independent Control Systems. In Seventh NASA Formal Methods Symposium, pages 248--262, Pasadena, CA, 2015. [ PDF ]
[18] 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, pages 189--202, September 2014. [ DOI  PDF ]
[19] 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 ]
[20] 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 ]
[21] 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 ]
[22] 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 ]
[23] Zhengjiang Hu, Shin-Cheng Mu, and Stephanie Weirich. Guest Editorial: Advanced programming techniques for construction of robust, generic and evolutionary programs. Progress in Informatics, (10):1--2, March 2013. [ DOI  http ]
[24] 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.
[25] Richard A. Eisenberg and Stephanie Weirich. Dependently typed programming with singletons. In Haskell Symposium, pages 117--130, Copenhagen, Denmark, September 2012. [ PDF ]
[26] Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. Journal of Functional Programming, 22(3):225--274, May 2012.
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] Umut A. Acar, James Cheney, and Stephanie Weirich. Editorial - Special issue dedicated to ICFP 2010. J. Funct. Program., 22(4-5):379--381, 2012. [ DOI ]
[32] Benjamin C. Pierce and Stephanie Weirich. Preface to Special Issue on the POPLMark Challenge. J. Autom. Reasoning, 49(3):301--302, 2012.
[33] 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 ]
[34] 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 ]
[35] 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 ]
[36] 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 ]
[37] Dimitrios Vytiniotis and Stephanie Weirich. Parametricity, Type Equality and Higher-order Polymorphism. Journal of Functional Programming, 20(2):175--210, March 2010. [ PDF  Abstract ]
[38] 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 ]
[39] 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 ]
[40] 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 ]
[41] 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 ]
[42] 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. [ PDF  Abstract ]
[43] 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. [ Project  PDF  Abstract ]
[44] 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 ]
[45] 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 ]
[46] 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. [ PDF  PS  Abstract ]
[47] 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 ]
[48] 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 ]
[49] Stephanie Weirich. Type-Safe Run-time Polytypic Programming. Journal of Functional Programming, 16(10):681--710, November 2006. [ PDF  Abstract ]
[50] 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. [ PDF  Abstract ]
[51] 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 ]
[52] 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 ]
[53] Stephanie Weirich. RepLib: A library for derivable type classes. In Haskell Workshop, pages 1--12, Portland, OR, USA, September 2006. [ Project  PDF  Abstract ]
[54] 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 ]
[55] 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 ]
[56] 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 ]
[57] 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 ]
[58] 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 ]
[59] 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 ]
[60] Stephanie Weirich. Type-Safe Cast. Journal of Functional Programming, 14(6):681--695, November 2004. [ PDF  Abstract ]
[61] 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 ]
[62] 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 ]
[63] 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 ]
[64] 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 ]
[65] 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 ]
[66] 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 ]
[67] 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 ]
[68] 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 ]
[69] 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 ]
[70] 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 ]
[71] 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 ]

Book Chapters
[1] Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis. A Reflection on Types. In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, editors, WadlerFest 2016: A list of successes that can change the world, LNCS, pages 292--317. Springer, 2016. [ DOI  PDF ]
[2] 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.
[3] 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 ]
[4] 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 ]

Misc
[1] Stephanie Weirich. Implementing Dependent Types in pi-forall, 2022. Lecture notes for the Oregon Programming Languages Summer School. [ DOI  http ]
[2] Stephanie Weirich and Benjamin Pierce. ICFP 2020 Post-Conference Report, 2021. [ arXiv  http ]
[3] Antal Spector-Zabusky, Joachim Breitner, Yao Li, and Stephanie Weirich. Embracing a mechanized formalization gap, October 2019. [ arXiv ]
[4] Anastasiya Kravchuk-Kirilyuk Stephanie Weirich, Antoine Voizard. Locally Nameless at Scale. The Fourth International Workshop on Coq for Programming Languages, January 2018. [ PDF ]
[5] Stephanie Weirich. The Influence of Dependent Types, January 2017. Invited keynote given at POPL 2017.
[6] Stephanie Weirich. Depending on Types, 2014. Invited keynote given at ICFP 2014.
[7] Stephanie Weirich. Designing Dependently-Typed Programming Languages. Lectures given at the Summer School on Logic and Theorem Proving in Programming Languages, Eugene OR, USA. July 2013, July 2013.
[8] Stephanie Weirich. Dependently typed programming in GHC, May 2012. Invited keynote given at FLOPS 2012.
[9] Kathleen Fisher, Ronald Garcia, and Stephanie Weirich. Nourishing the future of the field: the programming language mentoring workshop 2012, April 2012. [ DOI ]
[10] Stephanie Weirich. Combining Proofs and Programs, June 2011. Joint invited speaker for Rewriting Techniques and Applications (RTA 2011) and Typed Lambda Calculi and Applications (TLCA 2011).
[11] Stephanie Weirich. ICFP 2010 PC Chair's Report, September 2010.
[12] Brian Aydemir and Stephanie Weirich. LNgen: Tool Support for Locally Nameless Representations, June 2010. [ Project  PDF ]
[13] Stephanie Weirich. Haskell 2009 PC Chair's Report, August 2009.
[14] Brian Aydemir, Steve Zdancewic, and Stephanie Weirich. Abstracting Syntax, March 2009. [ Project  PDF ]
[15] Brian Aydemir, Aaron Bohannon, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, Stephanie Weirich, and Steve Zdancewic. Using Proof Assistants for Programming Language Research or, How to write your Next POPL paper in Coq. Tutorial session co-located with POPL 2008, San Francisco, CA, January 2008. Tutorial materials available at http://www.cis.upenn.edu/~plclub/popl08-tutorial/.
[16] Stephanie Weirich and Brian Aydemir. Coq for Programming Language Metatheory. Lectures given at the Summer School on Logic and Theorem Proving in Programming Languages, Eugene OR, USA. July 22-25, 2008, 2008. Tutorial materials available at http://www.cis.upenn.edu/~plclub/oregon08/.
[17] Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. Manifest Security, January 2007. White paper. [ PDF ]

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

Artifacts, Extended Versions, and Technical Reports
[1] Yao Li and Stephanie Weirich. Program Adverbs and Tlön Embeddings (artifact). Technical report, June 2022. Awarded "Available" and "Evaluated & Reusable" badges by ICFP 2021 Artifact Evaluation Committee. [ DOI ]
[2] Pritam Choudhury, Harley Eades III, and Stephanie Weirich. Artifact Associated with A Dependent Dependency Calculus. Technical report, January 2022. Awarded "Reusable" and "Available" badges by ESOP 2022 Artifact Evaluation Committee. [ DOI ]
[3] Yao Li, Li yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths (artifact). Technical report, May 2021. Awarded "Functional" and "Available" badges by ICFP 2021 Artifact Evaluation Committee. [ DOI ]
[4] Yao Li, Li yao Xia, and Stephanie Weirich. Reasoning about the garden of forking paths. Technical report, March 2021. [ arXiv ]
[5] Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. Artifact for "A Graded Dependent Type System with a Usage-Aware Semantics". Technical report, December 2020. Awarded "Reusable", "Functional" and "Available" badges by POPL 2021 Artifact Evaluation Committee. [ DOI ]
[6] Pritam Choudhury, Harley D. Eades III, Richard A. Eisenberg, and Stephanie Weirich. A Graded Dependent Type System with a Usage-Aware Semantics (Extended Version). Technical report, 2020. [ http ]
[7] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. Replication Package for Article: A Role for Dependent Types in Haskell. Technical report, July 2019. Awarded "Functional" and "Available" badges by ICFP 2019 Artifact Evaluation Committee. [ DOI ]
[8] Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg. A Role for Dependent Types in Haskell (Extended Version). Technical report, 2019. [ http ]
[9] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, and Stephanie Weirich. The hs-to-coq tool with examples. Technical report, July 2018. Awarded "Artifacts Available" and "Artifacts Evaluated - Functional" badges by ICFP 2018 Artifact Evaluation Committee. [ DOI ]
[10] Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed. Visible Type Application (Extended version). Technical report, January 2016. [ PDF ]
[11] Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence (Extended Version). Technical Report MS-CIS-14-10, University of Pennsylvania, October 2014. [ PDF ]
[12] 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 ]
[13] 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 ]
[14] 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 ]
[15] Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. System FC with explicit kind equality (Extended Version). Technical report, September 2013. [ PDF ]
[16] 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 ]
[17] 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 ]
[18] 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. [ PDF ]
[19] 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. [ PDF ]
[20] 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 ]
[21] 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 ]
[22] 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 ]
[23] 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 ]
[24] 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  Abstract ]
[25] 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 ]
[26] 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. [ PDF  Abstract ]
[27] Geoffrey Washburn and Stephanie Weirich. Unifying nominal and structural ad-hoc polymorphism (Extended version). Technical report, University of Pennsylvania, March 2004. [ PDF  Abstract ]
[28] 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 ]
[29] Michael Hicks and Stephanie Weirich. A Calculus for Dynamic Loading. Technical Report MS-CIS-00-07, University of Pennsylvania, April 2000. [ PDF  Abstract ]
[30] 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: Tue Feb 14 10:34:12 EST 2023