Static Debugging: Browsing the Web of Program Invariants. - Cormac Flanagan; Matthew Flatt; Shriram Krishnamurthi; Stephanie Weirich; Matthias Felleisen (PLDI, 1996)

Flexible Type Analysis. - Karl Crary; Stephanie Weirich (ICFP, 1999)

Type-safe cast: functional pearl. - Stephanie Weirich (ICFP, 2000)

Resource Bound Certification. - Karl Crary; Stephanie Weirich (POPL, 2000)

Safe and Flexible Dynamic Linking of Native Code. - Michael W. Hicks; Stephanie Weirich; Karl Crary (Types in Compilation, 2000)

Encoding Intensional Type Analysis. - Stephanie Weirich (ESOP, 2001)

Higher-Order Intensional Type Analysis. - Stephanie Weirich (ESOP, 2002)

Intensional polymorphism in type-erasure semantics. - Karl Crary; Stephanie Weirich; J. Gregory Morrisett (J. Funct. Program., 2002)

Programming with Types. - Stephanie Weirich (2002)

A Design for Type-Directed Programming in Java. - Stephanie Weirich; Liang Huang 001 (WOOD, 2004)

Type-safe cast. - Stephanie Weirich (J. Funct. Program., 2004)

PolyAML: a polymorphic aspect-oriented functional programming language. - Daniel S. Dantas; David Walker 001; Geoffrey Washburn; Stephanie Weirich (ICFP, 2005)

Generalizing Parametricity Using Information-flow. - Geoffrey Washburn; Stephanie Weirich (LICS, 2005)

An open and shut typecase. - Dimitrios Vytiniotis; Geoffrey Washburn; Stephanie Weirich (TLDI, 2005)

Mechanized Metatheory for the Masses: The PoplMark Challenge. - Brian E. Aydemir; Aaron Bohannon; Matthew Fairbairn; J. Nathan Foster; Benjamin C. Pierce; Peter Sewell; Dimitrios Vytiniotis; Geoffrey Washburn; Stephanie Weirich; Steve Zdancewic (TPHOLs, 2005)

It Is Time to Mechanize Programming Language Metatheory. - Benjamin C. Pierce; Peter Sewell; Stephanie Weirich; Steve Zdancewic (VSTTE, 2005)

RepLib: a library for derivable type classes. - Stephanie Weirich (Haskell, 2006)

Simple unification-based type inference for GADTs. - Simon L. Peyton Jones; Dimitrios Vytiniotis; Stephanie Weirich; Geoffrey Washburn (ICFP, 2006)

Boxy types: inference for higher-rank types and impredicativity. - Dimitrios Vytiniotis; Stephanie Weirich; Simon L. Peyton Jones (ICFP, 2006)

Good advice for type-directed programming aspect-oriented programming and extensible generic functions. - Geoffrey Washburn; Stephanie Weirich (ICFP-WGP, 2006)

Nominal Reasoning Techniques in Coq: (Extended Abstract). - Brian E. Aydemir; Aaron Bohannon; Stephanie Weirich (LFMTP@FLoC, 2006)

Type-safe run-time polytypic programming. - Stephanie Weirich (J. Funct. Program., 2006)

Free Theorems and Runtime Type Representations. - Dimitrios Vytiniotis; Stephanie Weirich (MFPS, 2007)

Practical type inference for arbitrary-rank types. - Simon L. Peyton Jones; Dimitrios Vytiniotis; Stephanie Weirich; Mark Shields (J. Funct. Program., 2007)

FPH: first-class polymorphism for Haskell. - Dimitrios Vytiniotis; Stephanie Weirich; Simon L. Peyton Jones (ICFP, 2008)

Engineering formal metatheory. - Brian E. Aydemir; Arthur Charguéraud; Benjamin C. Pierce; Randy Pollack; Stephanie Weirich (POPL, 2008)

Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. - Geoffrey Washburn; Stephanie Weirich (J. Funct. Program., 2008)

AspectML: A polymorphic aspect-oriented functional programming language. - Daniel S. Dantas; David Walker 001; Geoffrey Washburn; Stephanie Weirich (ACM Trans. Program. Lang. Syst., 2008)

Reactive noninterference. - Aaron Bohannon; Benjamin C. Pierce; Vilhelm Sjöberg; Stephanie Weirich; Steve Zdancewic (CCS, 2009)

Haskell Symposium Program Chair's Report. - Stephanie Weirich (Haskell, 2009)

Arity-generic datatype-generic programming: (abstract only). - Stephanie Weirich; Chris Casinghino (ACM SIGPLAN Notices, 2009)

Arity-generic datatype-generic programming. - Stephanie Weirich; Chris Casinghino (PLPV, 2010)

Dependent types and program equivalence. - Limin Jia 001; Jianzhou Zhao; Vilhelm Sjöberg; Stephanie Weirich (POPL, 2010)

Language-based verification will change the world. - Tim Sheard; Aaron Stump; Stephanie Weirich (FoSER, 2010)

Generic Programming with Dependent Types. - Stephanie Weirich; Chris Casinghino (SSGIP, 2010)

Termination Casts: A Flexible Approach to Termination with General Recursion - Aaron Stump; Vilhelm Sjöberg; Stephanie Weirich (PAR, 2010)

Parametricity, type equality, and higher-order polymorphism. - Dimitrios Vytiniotis; Stephanie Weirich (J. Funct. Program., 2010)

Binders unbound. - Stephanie Weirich; Brent A. Yorgey; Tim Sheard (ICFP, 2011)

Generative type abstraction and type-level computation. - Stephanie Weirich; Dimitrios Vytiniotis; Simon L. Peyton Jones; Steve Zdancewic (POPL, 2011)

Combining Proofs and Programs. - Stephanie Weirich (TLCA, 2011)

Dependently Typed Programming (NII Shonan Meeting 2011-3). - Shin-Cheng Mu; Conor McBride; Stephanie Weirich (NII Shonan Meet. Rep., 2011)

Dependently-Typed Programming in GHC. - Stephanie Weirich (FLOPS, 2012)

Dependently typed programming with singletons. - Richard A. Eisenberg; Stephanie Weirich (Haskell, 2012)

Equational reasoning about programs with general recursion and call-by-value semantics. - Garrin Kimmell; Aaron Stump; Harley D. Eades III; Peng Fu 001; Tim Sheard; Stephanie Weirich; Chris Casinghino; Vilhelm Sjöberg; Nathan Collins; Ki Yung Ahn (PLPV, 2012)

Giving Haskell a promotion. - Brent A. Yorgey; Stephanie Weirich; Julien Cretin; Simon L. Peyton Jones; Dimitrios Vytiniotis; José Pedro Magalhães (TLDI, 2012)

Step-Indexed Normalization for a Language with General Recursion - Chris Casinghino; Vilhelm Sjöberg; Stephanie Weirich (MSFP, 2012)

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems - Vilhelm Sjöberg; Chris Casinghino; Ki Yung Ahn; Nathan Collins; Harley D. Eades III; Peng Fu 001; Garrin Kimmell; Tim Sheard; Aaron Stump; Stephanie Weirich (MSFP, 2012)

Preface. - Benjamin C. Pierce; Stephanie Weirich (J. Autom. Reason., 2012)

Editorial - Special issue dedicated to ICFP 2010. - Umut A. Acar; James Cheney; Stephanie Weirich (J. Funct. Program., 2012)

Contracts made manifest. - Michael Greenberg 002; Benjamin C. Pierce; Stephanie Weirich (J. Funct. Program., 2012)

Nourishing the future of the field: the programming language mentoring workshop 2012. - Kathleen Fisher; Ronald Garcia; Stephanie Weirich (ACM SIGPLAN Notices, 2012)

Towards synthesis of platform-aware attack-resilient control systems: extended abstract. - Miroslav Pajic; Nicola Bezzo; James Weimer; Rajeev Alur; Rahul Mangharam; Nathan Michael; George J. Pappas; Oleg Sokolsky; Paulo Tabuada; Stephanie Weirich; Insup Lee 001 (HiCoNS, 2013)

System FC with explicit kind equality. - Stephanie Weirich; Justin Hsu; Richard A. Eisenberg (ICFP, 2013)

Type Systems. - Stephanie Weirich (Computing Handbook, 3rd ed. (1), 2014)

Depending on types. - Stephanie Weirich (ICFP, 2014)

Combining proofs and programs in a dependently typed language. - Chris Casinghino; Vilhelm Sjöberg; Stephanie Weirich (POPL, 2014)

Closed type families with overlapping equations. - Richard A. Eisenberg; Dimitrios Vytiniotis; Simon L. Peyton Jones; Stephanie Weirich (POPL, 2014)

Verified ROS-Based Deployment of Platform-Independent Control Systems. - Wenrui Meng; Junkil Park; Oleg Sokolsky; Stephanie Weirich; Insup Lee 001 (NFM, 2015)

Programming up to Congruence. - Vilhelm Sjöberg; Stephanie Weirich (POPL, 2015)

How to write a good research paper. - Stephanie Weirich (PLMW@POPL, 2015)

How to give a good research talk. - Stephanie Weirich (PLMW@POPL, 2015)

A Reflection on Types. - Simon Peyton Jones; Stephanie Weirich; Richard A. Eisenberg; Dimitrios Vytiniotis (A List of Successes That Can Change the World, 2016)

Visible Type Application. - Richard A. Eisenberg; Stephanie Weirich; Hamidhasan G. Ahmed (ESOP, 2016)

Needle & Knot: Binder Boilerplate Tied Up. - Steven Keuchel; Stephanie Weirich; Tom Schrijvers (ESOP, 2016)

Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). - Marco Gaboardi; Suresh Jagannathan; Ranjit Jhala; Stephanie Weirich (Dagstuhl Reports, 2016)

Safe zero-cost coercions for Haskell. - Joachim Breitner; Richard A. Eisenberg; Simon Peyton Jones; Stephanie Weirich (J. Funct. Program., 2016)

The influence of dependent types (keynote). - Stephanie Weirich (POPL, 2017)

A specification for dependent types in Haskell. - Stephanie Weirich; Antoine Voizard; Pedro Henrique Azevedo de Amorim; Richard A. Eisenberg (Proc. ACM Program. Lang., 2017)

Total Haskell is reasonable Coq. - Antal Spector-Zabusky; Joachim Breitner; Christine Rizkallah; Stephanie Weirich (CPP, 2018)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (CoRR, 2018)

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (Proc. ACM Program. Lang., 2018)

Eta-Equivalence in Core Dependent Haskell. - Anastasiya Kravchuk-Kirilyuk; Antoine Voizard; Stephanie Weirich (TYPES, 2019)

A Role for Dependent Types in Haskell (Extended version). - Stephanie Weirich; Pritam Choudhury; Antoine Voizard; Richard A. Eisenberg (CoRR, 2019)

Embracing a mechanized formalization gap. - Antal Spector-Zabusky; Joachim Breitner; Yao Li 004; Stephanie Weirich (CoRR, 2019)

A role for dependent types in Haskell. - Stephanie Weirich; Pritam Choudhury; Antoine Voizard; Richard A. Eisenberg (Proc. ACM Program. Lang., 2019)

A graded dependent type system with a usage-aware semantics (extended version). - Pritam Choudhury; Harley Eades III; Richard A. Eisenberg; Stephanie C. Weirich (CoRR, 2020)

ICFP 2020 Post-Conference Report. - Stephanie Weirich; Benjamin C. Pierce (CoRR, 2021)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)

A graded dependent type system with a usage-aware semantics. - Pritam Choudhury; Harley Eades III; Richard A. Eisenberg; Stephanie Weirich (Proc. ACM Program. Lang., 2021)

An existential crisis resolved: type inference for first-class existential types. - Richard A. Eisenberg; Guillaume Duboc; Stephanie Weirich; Daniel Lee (Proc. ACM Program. Lang., 2021)

Reasoning about the garden of forking paths. - Yao Li 004; Li-yao Xia; Stephanie Weirich (Proc. ACM Program. Lang., 2021)

A Dependent Dependency Calculus. - Pritam Choudhury; Harley Eades III; Stephanie Weirich (ESOP, 2022)

A Dependent Dependency Calculus (Extended Version). - Pritam Choudhury; Harley Eades III; Stephanie Weirich (CoRR, 2022)

Implementing Dependent Types in pi-forall. - Stephanie Weirich (CoRR, 2022)

Program adverbs and Tlön embeddings. - Yao Li 004; Stephanie Weirich (Proc. ACM Program. Lang., 2022)

Making Logical Relations More Relatable (Proof Pearl). - Emmanuel Suárez Acevedo; Stephanie Weirich (CoRR, 2023)

Effects and Coeffects in Call-By-Push-Value (Extended Version). - Cassia Torczon; Emmanuel Suárez Acevedo; Shubh Agrawal; Joey Velez-Ginorio; Stephanie Weirich (CoRR, 2023)

Dependently-Typed Programming with Logical Equality Reflection. - Yiyun Liu; Stephanie Weirich (Proc. ACM Program. Lang., 2023)

Effects and Coeffects in Call-by-Push-Value. - Cassia Torczon; Emmanuel Suárez Acevedo; Shubh Agrawal; Joey Velez-Ginorio; Stephanie Weirich (Proc. ACM Program. Lang., 2024)

Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. - Li-yao Xia; Laura Israel; Maite Kramarz; Nicholas Coltharp; Koen Claessen; Stephanie Weirich; Yao Li 004 (Proc. ACM Program. Lang., 2024)

Internalizing Indistinguishability with Dependent Types. - Yiyun Liu; Jonathan Chan 002; Jessica Shi 002; Stephanie Weirich (Proc. ACM Program. Lang., 2024)

Stratified Type Theory. - Jonathan Chan 002; Stephanie Weirich (ESOP (1), 2025)

Consistency of a Dependent Calculus of Indistinguishability. - Yiyun Liu; Jonathan Chan 002; Stephanie Weirich (Proc. ACM Program. Lang., 2025)

Bounded First-Class Universe Levels in Dependent Type Theory. - Jonathan Chan 002; Stephanie Weirich (CoRR, 2025)