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

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

Ironclad C++: a library-augmented type-safe subset of c++. - Christian DeLozier; Richard A. Eisenberg; Santosh Nagarakatte; Peter-Michael Osera; Milo M. K. Martin; Steve Zdancewic (OOPSLA, 2013)

Promoting functions to type families in Haskell. - Richard A. Eisenberg; Jan Stolarek (Haskell, 2014)

Experience report: type-checking polymorphic units for astrophysics research in Haskell. - Takayuki Muranushi; Richard A. Eisenberg (Haskell, 2014)

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

Injective type families for Haskell. - Jan Stolarek; Simon L. Peyton Jones; Richard A. Eisenberg (Haskell, 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)

Pattern synonyms. - Matthew Pickering; Gergo Érdi; Simon Peyton Jones; Richard A. Eisenberg (Haskell, 2016)

Dependent Types in Haskell: Theory and Practice. - Richard A. Eisenberg (CoRR, 2016)

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

Levity polymorphism. - Richard A. Eisenberg; Simon Peyton Jones (PLDI, 2017)

Constrained type families. - J. Garrett Morris; Richard A. Eisenberg (Proc. ACM Program. Lang., 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)

Type variables in patterns. - Richard A. Eisenberg; Joachim Breitner; Simon Peyton Jones (Haskell@ICFP, 2018)

The Thoralf plugin: for your fancy type needs. - Divesh Otwani; Richard A. Eisenberg (Haskell@ICFP, 2018)

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

Kind Inference for Datatypes: Technical Supplement. - Ningning Xie; Richard A. Eisenberg; Bruno C. d. S. Oliveira (CoRR, 2019)

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

Stitch: the sound type-indexed type checker (functional pearl). - Richard A. Eisenberg (Haskell@ICFP, 2020)

Composing effects into tasks and workflows. - Yves Parès; Jean-Philippe Bernardy; Richard A. Eisenberg (Haskell@ICFP, 2020)

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)

Kinds are calling conventions. - Paul Downen; Zena M. Ariola; Simon Peyton Jones; Richard A. Eisenberg (Proc. ACM Program. Lang., 2020)

Partial type constructors: or, making ad hoc datatypes less ad hoc. - Mark P. Jones; J. Garrett Morris; Richard A. Eisenberg (Proc. ACM Program. Lang., 2020)

Kind inference for datatypes. - Ningning Xie; Richard A. Eisenberg; Bruno C. d. S. Oliveira (Proc. ACM Program. Lang., 2020)

Seeking stability by being lazy and shallow: lazy and shallow instantiation is user friendly. - Gert-Jan Bottu; Richard A. Eisenberg (Haskell, 2021)

Linear Constraints. - Jean-Philippe Bernardy; Richard A. Eisenberg; Csongor Kiss; Arnaud Spiwack; Nicolas Wu (CoRR, 2021)

Seeking Stability by being Lazy and Shallow. - Gert-Jan Bottu; Richard A. Eisenberg (CoRR, 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)

Eiger: Auditable, executable, flexible legal regulations. - Alexander Bernauer; Richard A. Eisenberg (CoRR, 2022)

Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation. - Faustyna Krawiec; Simon Peyton Jones; Neel Krishnaswami; Tom Ellis; Richard A. Eisenberg; Andrew W. Fitzgibbon (Proc. ACM Program. Lang., 2022)

Linearly qualified types: generic inference for capabilities and uniqueness. - Arnaud Spiwack; Csongor Kiss; Jean-Philippe Bernardy; Nicolas Wu; Richard A. Eisenberg (Proc. ACM Program. Lang., 2022)

Oxidizing OCaml with Modal Memory Management. - Anton Lorenzen; Leo White; Stephen Dolan; Richard A. Eisenberg; Sam Lindley (Proc. ACM Program. Lang., 2024)

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; Derek Dreyer (Proc. ACM Program. Lang., 2025)