Refereed Journal, Conference and Workshop Publications
|
[1]
|
Jonathan Chan and Stephanie Weirich.
Stratified Type Theory.
In Viktor Vafeiadis, editor, European Symposium on Programming
Languages and Systems, ESOP 2025, May 2025.
To appear.
|
|
[2]
|
Yiyun Liu, Jonathan Chan, and Stephanie Weirich.
Consistency of a Dependent Calculus of Indistinguishability.
Proc. ACM Program. Lang., (POPL), January 2025.
Conditionally accepted to POPL 2025.
|
|
[3]
|
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey
Velez-Ginorio, and Stephanie Weirich.
Effects and Coeffects in Call-By-Push-Value.
Proc. ACM Program. Lang., 8(OOPSLA), October 2024.
[ DOI
Abstract ]
|
|
[4]
|
Li-Yao Xia, Laura Israel, Maite Kramarz, Nathan Coltharp, Koen Claessen,
Stephanie Weirich, and Yao Li.
Story of Your Lazy Function's Life: A Bidirectional Demand
Semantics for Mechanized Cost Analysis of Lazy Programs.
Proc. ACM Program. Lang., 8(ICFP), August 2024.
[ DOI
PDF
Abstract ]
|
|
[5]
|
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich.
Internalizing Indistinguishability with Dependent Types.
Proc. ACM Program. Lang., 8(POPL), January 2024.
[ DOI
PDF
Abstract ]
|
|
[6]
|
Yiyun Liu and Stephanie Weirich.
Dependently-Typed Programming with Logical Equality Reflection.
Proc. ACM Program. Lang., 7(ICFP), August 2023.
[ DOI
PDF
Abstract ]
|
|
[7]
|
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
Abstract ]
|
|
[8]
|
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 ]
|
|
[9]
|
Yao Li, Li-yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths.
Proc. ACM Program. Lang., 5(ICFP), August 2021.
[ DOI
PDF
Abstract ]
|
|
[10]
|
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
Abstract ]
|
|
[11]
|
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 ]
|
|
[12]
|
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 ]
|
|
[13]
|
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, sep 2020. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik.
[ DOI
http ]
|
|
[14]
|
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 ]
|
|
[15]
|
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 ]
|
|
[16]
|
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 ]
|
|
[17]
|
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 ]
|
|
[18]
|
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 ]
|
|
[19]
|
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 ]
|
|
[20]
|
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 ]
|
|
[21]
|
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 ]
|
|
[22]
|
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 ]
|
|
[23]
|
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 ]
|
|
[24]
|
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 ]
|
|
[25]
|
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich.
Combining Proofs and Programs in a Dependently Typed Language.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, page 33–45, New York, NY,
USA, 2014. Association for Computing Machinery.
[ DOI
.pdf
Abstract ]
|
|
[26]
|
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 ]
|
|
[27]
|
Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie
Weirich.
Safe Zero-Cost Coercions for Haskell.
In Proceedings of the 19th ACM SIGPLAN International Conference
on Functional Programming, ICFP '14, page 189–202, New York, NY, USA,
2014. Association for Computing Machinery.
[ DOI
http
Abstract ]
|
|
[28]
|
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 ]
|
|
[29]
|
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 ]
|
|
[30]
|
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.
|
|
[31]
|
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, page 275–286, New York, NY, USA,
2013. Association for Computing Machinery.
[ DOI
PDF
http
Abstract ]
|
|
[32]
|
Richard A. Eisenberg and Stephanie Weirich.
Dependently typed programming with singletons.
In Haskell Symposium, pages 117--130, Copenhagen, Denmark,
September 2012.
[ PDF ]
|
|
[33]
|
Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.
Contracts made manifest.
Journal of Functional Programming, 22(3):225--274, May 2012.
|
|
[34]
|
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 ]
|
|
[35]
|
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 ]
|
|
[36]
|
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 ]
|
|
[37]
|
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 ]
|
|
[38]
|
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 ]
|
|
[39]
|
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 ]
|
|
[40]
|
Benjamin C. Pierce and Stephanie Weirich.
Preface to Special Issue on the POPLMark Challenge.
J. Autom. Reasoning, 49(3):301--302, 2012.
|
|
[41]
|
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 ]
|
|
[42]
|
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 ]
|
|
[43]
|
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 ]
|
|
[44]
|
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 ]
|
|
[45]
|
Dimitrios Vytiniotis and Stephanie Weirich.
Parametricity, Type Equality and Higher-order Polymorphism.
Journal of Functional Programming, 20(2):175--210, March 2010.
[ PDF
Abstract ]
|
|
[46]
|
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 ]
|
|
[47]
|
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 ]
|
|
[48]
|
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 ]
|
|
[49]
|
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 ]
|
|
[50]
|
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 ]
|
|
[51]
|
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 ]
|
|
[52]
|
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 ]
|
|
[53]
|
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 ]
|
|
[54]
|
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 ]
|
|
[55]
|
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 ]
|
|
[56]
|
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 ]
|
|
[57]
|
Stephanie Weirich.
Type-Safe Run-time Polytypic Programming.
Journal of Functional Programming, 16(10):681--710, November
2006.
[ PDF
Abstract ]
|
|
[58]
|
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 ]
|
|
[59]
|
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 ]
|
|
[60]
|
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 ]
|
|
[61]
|
Stephanie Weirich.
RepLib: A library for derivable type classes.
In Haskell Workshop, pages 1--12, Portland, OR, USA, September
2006.
[ Project
PDF
Abstract ]
|
|
[62]
|
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 ]
|
|
[63]
|
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 ]
|
|
[64]
|
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 ]
|
|
[65]
|
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 ]
|
|
[66]
|
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 ]
|
|
[67]
|
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 ]
|
|
[68]
|
Stephanie Weirich.
Type-Safe Cast.
Journal of Functional Programming, 14(6):681--695, November
2004.
[ PDF
Abstract ]
|
|
[69]
|
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 ]
|
|
[70]
|
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 ]
|
|
[71]
|
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 ]
|
|
[72]
|
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 ]
|
|
[73]
|
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 ]
|
|
[74]
|
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 ]
|
|
[75]
|
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 ]
|
|
[76]
|
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 ]
|
|
[77]
|
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 ]
|
|
[78]
|
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 ]
|
|
[79]
|
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 ]
|
|
[80]
|
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 ]
|
|
Artifacts, Extended Versions, and Technical Reports
|
[1]
|
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey
Velez-Ginorio, and Stephanie Weirich.
Artifact associated with "Effects and Coeffects in
Call-By-Push-Value".
Technical report, July 2024.
Awarded “Available”, “Evaluated & Reusable” and “Results
Reproduced” by OOPSLA 2024 Artifact Evaluation Committee.
[ DOI
http ]
|
|
[2]
|
Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen,
Stephanie Weirich, and Yao Li.
Story of Your Lazy Function's Life: A Bidirectional Demand
Semantics for Mechanized Cost Analysis of Lazy Programs (Artifact).
Technical report, June 2024.
[ DOI
http ]
|
|
[3]
|
Yiyun Liu, Jonathan Chan, Jessica Shi, and Stephanie Weirich.
Artifact associated with Internalizing Indistinguishability
with Dependent Types.
Technical report, October 2023.
Awarded “Available” and “Evaluated & Reusable” badges by POPL
2024 Artifact Evaluation Committee.
[ DOI
http ]
|
|
[4]
|
Yiyun Liu and Stephanie Weirich.
Artifact Associated with Dependently-Typed Programming with
Logical Equality Reflection.
Technical report, 2023.
Awarded “Available” and “Evaluated & Reusable” badges by ICFP
2023 Artifact Evaluation Committee.
[ DOI
http
Abstract ]
|
|
[5]
|
Yao Li and Stephanie Weirich.
Program Adverbs and Tlön Embeddings (artifact).
Technical report, June 2022.
Awarded “Available” and “Evaluated & Reusable” badges by ICFP
2023 Artifact Evaluation Committee.
[ DOI ]
|
|
[6]
|
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 ]
|
|
[7]
|
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 ]
|
|
[8]
|
Yao Li, Li-yao Xia, and Stephanie Weirich.
Reasoning about the garden of forking paths.
Technical report, March 2021.
[ arXiv
http ]
|
|
[9]
|
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 ]
|
|
[10]
|
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 ]
|
|
[11]
|
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 ]
|
|
[12]
|
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard Eisenberg.
A Role for Dependent Types in Haskell (Extended Version).
Technical report, 2019.
[ http ]
|
|
[13]
|
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 ]
|
|
[14]
|
Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan G. Ahmed.
Visible Type Application (Extended version).
Technical report, January 2016.
[ PDF ]
|
|
[15]
|
Vilhelm Sjöberg and Stephanie Weirich.
Programming up to Congruence (Extended Version).
Technical Report MS-CIS-14-10, University of Pennsylvania, October
2014.
[ PDF ]
|
|
[16]
|
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 ]
|
|
[17]
|
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 ]
|
|
[18]
|
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 ]
|
|
[19]
|
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
System FC with explicit kind equality (Extended Version).
Technical report, September 2013.
[ PDF ]
|
|
[20]
|
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 ]
|
|
[21]
|
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 ]
|
|
[22]
|
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 ]
|
|
[23]
|
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 ]
|
|
[24]
|
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 ]
|
|
[25]
|
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 ]
|
|
[26]
|
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 ]
|
|
[27]
|
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 ]
|
|
[28]
|
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 ]
|
|
[29]
|
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 ]
|
|
[30]
|
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 ]
|
|
[31]
|
Geoffrey Washburn and Stephanie Weirich.
Unifying nominal and structural ad-hoc polymorphism (Extended
version).
Technical report, University of Pennsylvania, March 2004.
[ PDF
Abstract ]
|
|
[32]
|
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 ]
|
|
[33]
|
Michael Hicks and Stephanie Weirich.
A Calculus for Dynamic Loading.
Technical Report MS-CIS-00-07, University of Pennsylvania, April
2000.
[ PDF
Abstract ]
|
|
[34]
|
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 ]
|
|