| 2025 | WoLLIC | Deep Induction for Inductive Families. | Patricia Johann, Edward Morehouse |
| 2022 | APLAS | Characterizing Functions Mappable over GADTs. | Patricia Johann, Pierre Cagne |
| 2022 | CPP | (Deep) induction rules for GADTs. | Patricia Johann, Enrico Ghiorzi |
| 2021 | FOSSACS | Parametricity for Primitive Nested Types. | Patricia Johann, Enrico Ghiorzi, Daniel Jeffries |
| 2020 | FOSSACS | Deep Induction: Induction Rules for (Truly) Nested Types. | Patricia Johann, Andrew Polonsky |
| 2020 | MFPS | Preface. | Patricia Johann |
| 2019 | LICS | Higher-Kinded Data Types: Syntax and Semantics. | Patricia Johann, Andrew Polonsky |
| 2018 | LICS | A General Framework for Relational Parametricity. | Kristina Sojakova, Patricia Johann |
| 2016 | LOPSTR | A Productivity Checker for Logic Programming. | Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt |
| 2015 | ICLP | Structural Resolution for Logic Programming. | Patricia Johann, Ekaterina Komendantskaya, Vladimir Komendantskiy |
| 2014 | POPL | A relationally parametric model of dependent type theory. | Robert Atkey, Neil Ghani, Patricia Johann |
| 2013 | POPL | Abstraction and invariance for algebraically indexed types. | Robert Atkey, Patricia Johann, Andrew Kennedy |
| 2012 | FOSSACS | Fibrational Induction Meets Effects. | Robert Atkey, Neil Ghani, Bart Jacobs, Patricia Johann |
| 2011 | CALCO | Indexed Induction and Coinduction, Fibrationally. | Clment Fumex, Neil Ghani, Patricia Johann |
| 2011 | FOSSACS | When Is a Type Refinement an Inductive Type? | Robert Atkey, Patricia Johann, Neil Ghani |
| 2010 | CSL | Fibrational Induction Rules for Initial Algebras. | Neil Ghani, Patricia Johann, Clment Fumex |
| 2010 | LICS | A Generic Operational Metatheory for Algebraic Effects. | Patricia Johann, Alex Simpson, Janis Voigtlnder |
| 2008 | POPL | Foundations for structured programming with GADTs. | Patricia Johann, Neil Ghani |
| 2005 | ICFP | Monadic augment and generalised short cut fusion. | Neil Ghani, Patricia Johann, Tarmo Uustalu, Varmo Vene |
| 2004 | POPL | Free theorems in the presence of | Patricia Johann, Janis Voigtlnder |
| 2003 | GPCE | Staged Notational Definitions. | Walid Taha, Patricia Johann |
| 1999 | SIGCSE | A funny thing happened on the way to the formula: demonstrating equality of functions and programs. | Patricia Johann |
| 1994 | CADE | Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. | Patricia Johann, Michael Kohlhase |
| 1992 | CADE | A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). | Daniel J. Dougherty, Patricia Johann |
| 1990 | CADE | An Improved General E-Unification Method. | Daniel J. Dougherty, Patricia Johann |