Stephanie Weirich

115 papers A* 12A 18B 2C 5Misc 1Journal 46Unranked 25

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach. Proc. ACM Program. Lang. Yiyun Liu, Stephanie Weirich
2026	J	`jnl`	Typing Strictness. Proc. ACM Program. Lang. Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich
2025	J	`jnl`	Bounded First-Class Universe Levels in Dependent Type Theory. CoRR Jonathan Chan, Stephanie Weirich
2025	J	`jnl`	Consistency of a Dependent Calculus of Indistinguishability. Proc. ACM Program. Lang. Yiyun Liu, Jonathan Chan, Stephanie Weirich
2025	C	`conf`	Rebound: Efficient, Expressive, and Well-Scoped Binding. Haskell Noé De Santo, Stephanie Weirich
2025	J	`jnl`	Rebound: Efficient, Expressive, and Well-Scoped Binding. CoRR Noé De Santo, Stephanie Weirich
2025	—	`conf`	Stratified Type Theory. ESOP (1) Jonathan Chan, Stephanie Weirich
2025	J	`jnl`	Typing Strictness (Extended Version). CoRR Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich
2024	J	`jnl`	Effects and Coeffects in Call-by-Push-Value. Proc. ACM Program. Lang. Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich
2024	J	`jnl`	Internalizing Indistinguishability with Dependent Types. Proc. ACM Program. Lang. Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich
2024	—	`ed.`	Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I ESOP (1) Stephanie Weirich
2024	—	`ed.`	Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part II ESOP (2) Stephanie Weirich
2024	J	`jnl`	Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. CoRR Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, Yao Li
2024	J	`jnl`	Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. Proc. ACM Program. Lang. Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, Yao Li
2023	J	`jnl`	Dependently-Typed Programming with Logical Equality Reflection. Proc. ACM Program. Lang. Yiyun Liu, Stephanie Weirich
2023	J	`jnl`	Effects and Coeffects in Call-By-Push-Value (Extended Version). CoRR Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich
2023	J	`jnl`	Making Logical Relations More Relatable (Proof Pearl). CoRR Emmanuel Suárez Acevedo, Stephanie Weirich
2023	J	`jnl`	Stratified Type Theory. CoRR Jonathan Chan, Stephanie Weirich
2022	J	`jnl`	A Dependent Dependency Calculus (Extended Version). CoRR Pritam Choudhury, Harley Eades III, Stephanie Weirich
2022	A	`conf`	A Dependent Dependency Calculus. ESOP Pritam Choudhury, Harley Eades III, Stephanie Weirich
2022	J	`jnl`	Implementing Dependent Types in pi-forall. CoRR Stephanie Weirich
2022	J	`jnl`	Program Adverbs and Tlön Embeddings. CoRR Yao Li, Stephanie Weirich
2022	J	`jnl`	Program adverbs and Tlön embeddings. Proc. ACM Program. Lang. Yao Li, Stephanie Weirich
2021	J	`jnl`	A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, Stephanie Weirich
2021	J	`jnl`	An existential crisis resolved: type inference for first-class existential types. Proc. ACM Program. Lang. Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, Daniel Lee
2021	J	`jnl`	ICFP 2020 Post-Conference Report. CoRR Stephanie Weirich, Benjamin C. Pierce
2021	J	`jnl`	Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. J. Funct. Program. Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, Stephanie Weirich
2021	J	`jnl`	Reasoning about the garden of forking paths. CoRR Yao Li, Li-yao Xia, Stephanie Weirich
2021	J	`jnl`	Reasoning about the garden of forking paths. Proc. ACM Program. Lang. Yao Li, Li-yao Xia, Stephanie Weirich
2019	J	`jnl`	A Role for Dependent Types in Haskell (Extended version). CoRR Stephanie Weirich, Pritam Choudhury, Antoine Voizard, Richard A. Eisenberg
2019	J	`jnl`	A role for dependent types in Haskell. Proc. ACM Program. Lang. Stephanie Weirich, Pritam Choudhury, Antoine Voizard, Richard A. Eisenberg
2019	J	`jnl`	Embracing a mechanized formalization gap. CoRR Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich
2019	—	`conf`	Eta-Equivalence in Core Dependent Haskell. TYPES Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich
2018	J	`jnl`	Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. CoRR Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
2018	J	`jnl`	Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). Proc. ACM Program. Lang. Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
2018	B	`conf`	Total Haskell is reasonable Coq. CPP Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
2017	J	`jnl`	A specification for dependent types in Haskell. Proc. ACM Program. Lang. Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, Richard A. Eisenberg
2017	A*	`conf`	The influence of dependent types (keynote). POPL Stephanie Weirich
2017	J	`jnl`	Total Haskell is Reasonable Coq. CoRR Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
2016	—	`conf`	A Reflection on Types. A List of Successes That Can Change the World Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, Dimitrios Vytiniotis
2016	J	`jnl`	Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). Dagstuhl Reports Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, Stephanie Weirich
2016	A	`conf`	Needle & Knot: Binder Boilerplate Tied Up. ESOP Steven Keuchel, Stephanie Weirich, Tom Schrijvers
2016	J	`jnl`	Safe zero-cost coercions for Haskell. J. Funct. Program. Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich
2016	A	`conf`	Visible Type Application. ESOP Richard A. Eisenberg, Stephanie Weirich, Hamidhasan G. Ahmed
2015	—	`conf`	How to give a good research talk. PLMW@POPL Stephanie Weirich
2015	—	`conf`	How to write a good research paper. PLMW@POPL Stephanie Weirich
2015	A*	`conf`	Programming up to Congruence. POPL Vilhelm Sjöberg, Stephanie Weirich
2015	—	`conf`	Verified ROS-Based Deployment of Platform-Independent Control Systems. NFM Wenrui Meng, Junkil Park, Oleg Sokolsky, Stephanie Weirich, Insup Lee
2014	A*	`conf`	Closed type families with overlapping equations. POPL Richard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich
2014	A*	`conf`	Combining proofs and programs in a dependently typed language. POPL Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
2014	A	`conf`	Depending on types. ICFP Stephanie Weirich
2014	A	`conf`	Safe zero-cost coercions for Haskell. ICFP Joachim Breitner, Richard A. Eisenberg, Simon L. Peyton Jones, Stephanie Weirich
2014	—	`ch.`	Type Systems. Computing Handbook, 3rd ed. (1) Stephanie Weirich
2013	—	`ed.`	Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013 DTP@ICFP Stephanie Weirich
2013	A	`conf`	System FC with explicit kind equality. ICFP Stephanie Weirich, Justin Hsu, Richard A. Eisenberg
2013	—	`conf`	Towards synthesis of platform-aware attack-resilient control systems: extended abstract. HiCoNS Miroslav Pajic, Nicola Bezzo, James Weimer, Rajeev Alur, Rahul Mangharam, Nathan Michael, George J. Pappas, Oleg Sokolsky, Paulo Tabuada, Stephanie Weirich, Insup Lee
2012	J	`jnl`	Contracts made manifest. J. Funct. Program. Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich
2012	C	`conf`	Dependently typed programming with singletons. Haskell Richard A. Eisenberg, Stephanie Weirich
2012	Misc	`conf`	Dependently-Typed Programming in GHC. FLOPS Stephanie Weirich
2012	J	`jnl`	Editorial - Special issue dedicated to ICFP 2010. J. Funct. Program. Umut A. Acar, James Cheney, Stephanie Weirich
2012	—	`conf`	Equational reasoning about programs with general recursion and call-by-value semantics. PLPV Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn
2012	—	`conf`	Giving Haskell a promotion. TLDI Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon L. Peyton Jones, Dimitrios Vytiniotis, José Pedro Magalhães
2012	—	`conf`	Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems MSFP Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
2012	J	`jnl`	Nourishing the future of the field: the programming language mentoring workshop 2012. ACM SIGPLAN Notices Kathleen Fisher, Ronald Garcia, Stephanie Weirich
2012	J	`jnl`	Preface. J. Autom. Reason. Benjamin C. Pierce, Stephanie Weirich
2012	—	`conf`	Step-Indexed Normalization for a Language with General Recursion MSFP Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
2011	A	`conf`	Binders unbound. ICFP Stephanie Weirich, Brent A. Yorgey, Tim Sheard
2011	—	`conf`	Combining Proofs and Programs. RTA Stephanie Weirich
2011	—	`conf`	Combining Proofs and Programs. TLCA Stephanie Weirich
2011	J	`jnl`	Dependently Typed Programming (NII Shonan Meeting 2011-3). NII Shonan Meet. Rep. Shin-Cheng Mu, Conor McBride, Stephanie Weirich
2011	A*	`conf`	Generative type abstraction and type-level computation. POPL Stephanie Weirich, Dimitrios Vytiniotis, Simon L. Peyton Jones, Steve Zdancewic
2011	—	`ed.`	Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Austin, TX, USA, January 25, 2011 TLDI Stephanie Weirich, Derek Dreyer
2010	—	`conf`	Arity-generic datatype-generic programming. PLPV Stephanie Weirich, Chris Casinghino
2010	A*	`conf`	Contracts made manifest. POPL Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich
2010	A*	`conf`	Dependent types and program equivalence. POPL Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich
2010	—	`conf`	Generic Programming with Dependent Types. SSGIP Stephanie Weirich, Chris Casinghino
2010	—	`conf`	Language-based verification will change the world. FoSER Tim Sheard, Aaron Stump, Stephanie Weirich
2010	J	`jnl`	Parametricity, type equality, and higher-order polymorphism. J. Funct. Program. Dimitrios Vytiniotis, Stephanie Weirich
2010	A	`ed.`	Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 ICFP Paul Hudak, Stephanie Weirich
2010	—	`conf`	Termination Casts: A Flexible Approach to Termination with General Recursion PAR Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
2010	—	`conf`	Termination Casts: A Flexible Approach to Termination with General Recursion. PAR@ITP Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
2009	J	`jnl`	Arity-generic datatype-generic programming: (abstract only). ACM SIGPLAN Notices Stephanie Weirich, Chris Casinghino
2009	C	`conf`	Haskell Symposium Program Chair's Report. Haskell Stephanie Weirich
2009	C	`ed.`	Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, Edinburgh, Scotland, UK, 3 September 2009 Haskell Stephanie Weirich
2009	A*	`conf`	Reactive noninterference. CCS Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, Steve Zdancewic
2008	J	`jnl`	AspectML: A polymorphic aspect-oriented functional programming language. ACM Trans. Program. Lang. Syst. Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich
2008	J	`jnl`	Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program. Geoffrey Washburn, Stephanie Weirich
2008	A*	`conf`	Engineering formal metatheory. POPL Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich
2008	A	`conf`	FPH: first-class polymorphism for Haskell. ICFP Dimitrios Vytiniotis, Stephanie Weirich, Simon L. Peyton Jones
2007	B	`conf`	Free Theorems and Runtime Type Representations. MFPS Dimitrios Vytiniotis, Stephanie Weirich
2007	J	`jnl`	Practical type inference for arbitrary-rank types. J. Funct. Program. Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields
2006	A	`conf`	Boxy types: inference for higher-rank types and impredicativity. ICFP Dimitrios Vytiniotis, Stephanie Weirich, Simon L. Peyton Jones
2006	—	`conf`	Good advice for type-directed programming aspect-oriented programming and extensible generic functions. ICFP-WGP Geoffrey Washburn, Stephanie Weirich
2006	—	`conf`	Nominal Reasoning Techniques in Coq: (Extended Abstract). LFMTP@FLoC Brian E. Aydemir, Aaron Bohannon, Stephanie Weirich
2006	C	`conf`	RepLib: a library for derivable type classes. Haskell Stephanie Weirich
2006	A	`conf`	Simple unification-based type inference for GADTs. ICFP Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Geoffrey Washburn
2006	J	`jnl`	Type-safe run-time polytypic programming. J. Funct. Program. Stephanie Weirich
2005	—	`conf`	An open and shut typecase. TLDI Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich
2005	A*	`conf`	Generalizing Parametricity Using Information-flow. LICS Geoffrey Washburn, Stephanie Weirich
2005	—	`conf`	It Is Time to Mechanize Programming Language Metatheory. VSTTE Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
2005	—	`conf`	Mechanized Metatheory for the Masses: The PoplMark Challenge. TPHOLs Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
2005	A	`conf`	Poly ICFP Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich
2004	—	`conf`	A Design for Type-Directed Programming in Java. WOOD Stephanie Weirich, Liang Huang
2004	J	`jnl`	Type-safe cast. J. Funct. Program. Stephanie Weirich
2003	A	`conf`	Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism. ICFP Geoffrey Washburn, Stephanie Weirich
2002	A	`conf`	Higher-Order Intensional Type Analysis. ESOP Stephanie Weirich
2002	J	`jnl`	Intensional polymorphism in type-erasure semantics. J. Funct. Program. Karl Crary, Stephanie Weirich, J. Gregory Morrisett
2002	—	`—`	Programming with Types. Stephanie Weirich
2001	A	`conf`	Encoding Intensional Type Analysis. ESOP Stephanie Weirich
2000	A*	`conf`	Resource Bound Certification. POPL Karl Crary, Stephanie Weirich
2000	—	`conf`	Safe and Flexible Dynamic Linking of Native Code. Types in Compilation Michael W. Hicks, Stephanie Weirich, Karl Crary
2000	A	`conf`	Type-safe cast: functional pearl. ICFP Stephanie Weirich
1999	A	`conf`	Flexible Type Analysis. ICFP Karl Crary, Stephanie Weirich
1998	A	`conf`	Intensional Polymorphism in Type-Erasure Semantics. ICFP Karl Crary, Stephanie Weirich, J. Gregory Morrisett
1996	A*	`conf`	Static Debugging: Browsing the Web of Program Invariants. PLDI Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, Matthias Felleisen