My publications are listed below in reverse chronological order.

• Data Race Freedom à la Mode. Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. Conditionally accepted at POPL 2025. (pdf)

1. Oxidizing OCaml with Modal Memory Management. Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, and Sam Lindley. ICFP 2024. (pdf)

2. Linearly qualified types: generic inference for capabilities and uniqueness. Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, and Richard A. Eisenberg. ICFP 2022. (pdf)

3. Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation. Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon. POPL 2022. (pdf)

4. An Existential Crisis Resolved: Type inference for first-class existential types. Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee. ICFP 2021. (pdf)

   Winner of Distinguished Paper Award.

5. Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly. Gert-Jan Bottu and Richard A. Eisenberg. Haskell Symposium 2021. (pdf)

6. A graded dependent type system with a usage-aware semantics. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. POPL 2021. (pdf extended pdf)

7. Kinds are Calling Conventions. Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. ICFP 2020. (pdf)

8. Stitch: The Sound Type-Indexed Type Checker, a Functional Pearl. Richard A. Eisenberg. Haskell Symposium 2020. (pdf tarball source repo slides from talk at NYC Haskell ZuriHac slides Haskell Symposium slides Haskell Symposium talk)

9. Composing Effects into Tasks and Workflows. Yves Parès, Jean-Philippe Bernardy, and Richard A. Eisenberg. Haskell Symposium 2020. (pdf source repo)

10. Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc. Mark P. Jones, J. Garrett Morris, and Richard A. Eisenberg. POPL 2020, New Orleans, LA, USA. (pdf extended pdf)

11. Kind Inference for Datatypes. Ningning Xie, Richard A. Eisenberg, and Bruno C. d. S. Oliveira. POPL 2020, New Orleans, LA, USA. (pdf supplement pdf)

    Winner of Distinguished Paper Award.

12. A Role for Dependent Types in Haskell. Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. ICFP 2019, Berlin, Germany. (pdf extended pdf)
13. Type Variables in Patterns. Richard A. Eisenberg, Joachim Breitner, and Simon Peyton Jones. Haskell Symposium 2018, St. Louis, MO, USA. (pdf extended pdf)
14. The Thoralf Plugin: For Your Fancy Type Needs. Divesh Otwani and Richard A. Eisenberg. Haskell Symposium 2018, St. Louis, MO, USA. (pdf)

15. Constrained Type Families. J. Garrett Morris and Richard A. Eisenberg. ICFP 2017, Oxford, UK. (pdf extended pdf)

16. A Specification for Dependently-Typed Haskell. Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. ICFP 2017, Oxford, UK. (pdf appendix pdf)

17. Levity Polymorphism. Richard A. Eisenberg and Simon Peyton Jones. PLDI 2017, Barcelona, Spain. (pdf extended pdf)

18. Safe Zero-cost Coercions for Haskell. Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. In the Journal of Functional Programming, vol. 26. Cambridge University Press, 2016. (pdf)

19. Pattern Synonyms. Matthew Pickering, Gergő Érdi, Simon Peyton Jones, Richard A. Eisenberg. Haskell Symposium 2016, Nara, Japan. (pdf extended pdf)

20. A Reflection on Types. Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, Dimitrios Vytiniotis. Wadlerfest 2016, Edinburgh, UK. (pdf)

21. Visible Type Application. Richard A. Eisenberg, Stephanie Weirich, and Hamidhasan Ahmed. ESOP 2016, Eindhoven, The Netherlands. (pdf extended pdf)

22. Injective Type Families for Haskell. Jan Stolarek, Simon Petyon Jones, and Richard A. Eisenberg. Haskell Symposium 2015, Vancouver, BC, Canada. (pdf)

    Injective Type Families for Haskell (extended version). Jan Stolarek, Simon Peyton Jones, and Richard A. Eisenberg. Politechnika Łódzka Technical Report, 2015. (pdf)

23. Promoting Functions to Type Families in Haskell. Richard A. Eisenberg and Jan Stolarek. Haskell Symposium 2014, Gothenburg, Sweden. (pdf extended pdf)

24. Experience Report: Type-checking Polymorphic Units for Astrophysics Research in Haskell. Takayuki Muranushi and Richard A. Eisenberg. Haskell Symposium 2014, Gothenburg, Sweden. (pdf)

25. Safe Zero-cost Coercions for Haskell. Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. ICFP 2014, Gothenburg, Sweden. (pdf)

    Safe Zero-cost Coercions for Haskell (Extended Version). Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Univ. of Pennsylvania Technical Report MS-CIS-14-07. 2014. (pdf) (NB: This has been superceded by the JFP version, above.)

26. Closed Type Families with Overlapping Equations. Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. POPL 2014, San Diego, CA, USA. (pdf)

    Closed Type Families with Overlapping Equations (Extended version). Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. Univ. of Pennsylvania Technical Report MS-CIS-13-10. 2013. (pdf)

27. Ironclad C++: A library-augmented type-safe subset of C++. Christian DeLozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. OOPSLA 2013, Indianapolis, IN, USA. (pdf technical report pdf)
28. System FC with Explicit Kind Equality. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. ICFP 2013, Boston, MA, USA. (pdf extended pdf)
29. Dependently Typed Programming with Singletons. Richard A. Eisenberg and Stephanie Weirich. Haskell Symposium 2012, Copenhagen, Denmark. (pdf)

Dependent Types in Haskell: Theory and Practice. Richard A. Eisenberg, PhD Thesis, University of Pennsylvania, 2016. (pdf)

1. Coercion Quantification. Ningning Xie and Richard A. Eisenberg. Haskell Implementors' Workshop 2018, St. Louis, MO, USA. (pdf)
2. Explaining Type Errors. Brent A. Yorgey, Richard A. Eisenberg, and Harley D. Eades III. Off the Beaten Track (OBT) 2018, Los Angeles, CA, USA. (pdf)

1. Eiger: Auditable, executable, flexible legal regulations. Presented at Haskell Symposium with Alexander Bernauer, September 16, 2022, Ljubljana, Slovenia. (pdf)

2. An Existential Crisis Resolved: Type Inference for First-Class Existential Types. Presented at ICFP, August 24, 2021, Online. (video)
3. Generalization is hard, but somebody's got to do it. Presented at Haskell Implementors' Workshop, August 22, 2021, Online. (video)
4. Simplifying Constraint Solving in GHC. Presented at Haskell eXchange, November 5, 2020, Online. (example code tarball)
5. Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc. Presented at MuniHac, September 11, 2020, Online. (slides)
6. Stitch: The Sound Type-Indexed Type Checker, a Functional Pearl. Presented at Haskell Symposium, August 28, 2020, Online. (slides video)
7. Parameters of Many Flavors. Presented at Haskell Love, August 1, 2020, Online. (slides/code)
8. Type Variables in Patterns. Presented at Haskell Symposium, September 28, 2018, St. Louis, MO, USA. (slides)
9. Constrained Type Families. Presented at ICFP, September 6, 2017, Oxford, UK. (slides YouTube)
10. Levity Polymorphism. Presented at PLDI, June 20, 2017, Barcelona, Spain. (slides YouTube)
11. A Dependent Haskell Triptych. Presented at Haskell Implementors' Workshop, September 24, 2016, Nara, Japan. (slides YouTube)
12. Visible Type Application. Presented at ESOP, April 4, 2016, Eindhoven, Netherlands. (slides)
13. Levity Polymorphism in Dependent Haskell. Presented at Haskell Implementors' Workshop, August 30, 2015, Vancouver, BC, Canada. (slides YouTube)
14. Dependent Haskell. Presented at Haskell Implementors' Workshop, September 6, 2014, Gothenburg, Sweden. (slides YouTube)
15. Safe Zero-cost Coercions for Haskell. Presented at ICFP, September 2, 2014, Gothenburg, Sweden. (slides YouTube)
16. Closed Type Families with Overlapping Equations. Presented at POPL, January 24, 2014, San Diego, CA, USA. (slides)
17. System FC with Explicit Kind Equality. Presented at ICFP, September 26, 2013, Boston, MA, USA. (slides)
18. GeneralizedNewtypeDeriving is now Type-Safe: How Roles Save the Day. Presented at Haskell Implementors' Workshop, September 22, 2013, Boston, MA, USA. (slides)
19. Dependently Typed Programming with Singletons. Presented at Haskell Symposium, September 13, 2012, Copenhagen, Denmark. (slides YouTube)

• Kind equalities in GHC, based on the ICFP'13 paper
• Visible type application in GHC, based on the POPL'16 submission
• Glambda, a lambda-calculus interpreter built with GADTs, useful as a case study
• A new Coercible solver, already part of GHC
• The units package, a domain-specific type system for dimensional analysis
• Roles, as based on the ICFP'14 paper, already part of GHC
• Closed type families, implemented in two major commits, as based on the POPL'14 paper
• The singletons library, which allows for automatic derivation of declarations that support dependent types in released versions of GHC

• Eiger: Auditable, executable, flexible legal regulations. Alexander Bernauer and Richard A. Eisenberg. Posted on arXiv and presented at Haskell Symposium 2022.
• System FC, as implemented in GHC. This is a summary of the internal language in GHC, as implemented. (pdf)

• An overabundance of equality: Implementing kind equalities into Haskell. Richard A. Eisenberg. (pdf)