A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract). - Daniel J. Dougherty; Patricia Johann (CADE, 1992)

An Improved General E-Unification Method. - Daniel J. Dougherty; Patricia Johann (J. Symb. Comput., 1992)

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. - Patricia Johann; Michael Kohlhase (CADE, 1994)

Solving Simplification Ordering Constraints. - Patricia Johann; Rolf Socher-Ambrosius (CCL, 1994)

Normal Forms in Combinatory Logic. - Patricia Johann (Notre Dame J. Formal Log., 1994)

A Combinatory Logic Approach to Higher-Order E-Unification. - Daniel J. Dougherty; Patricia Johann (Theor. Comput. Sci., 1995)

Deduction systems. - Rolf Socher-Ambrosius; Patricia Johann (Springer, 1997)

A funny thing happened on the way to the formula: demonstrating equality of functions and programs. - Patricia Johann (ITiCSE-WGR, 1999)

Warm fusion in Stratego: A case study in generation of program transformation systems. - Patricia Johann; Eelco Visser (Ann. Math. Artif. Intell., 2000)

Testing and enhancing a prototype program fusion engine. - Patricia Johann (ACM SIGSOFT Softw. Eng. Notes, 2000)

Short Cut Fusion: Proved and Improved. - Patricia Johann (SAIG, 2001)

Lumberjack Summer Camp: A Cross-Institutional Undergraduate Research Experience in Computer Science. - Patricia Johann; Franklyn A. Turbak (Comput. Sci. Educ., 2001)

Fusing Logic and Control with Local Transformations: An Example Optimization. - Patricia Johann; Eelco Visser (WRS, 2001)

A Generalization of Short-Cut Fusion and its Correctness Proof. - Patricia Johann (High. Order Symb. Comput., 2002)

Staged Notational Definitions. - Walid Taha; Patricia Johann (GPCE, 2003)

Short cut fusion is correct. - Patricia Johann (J. Funct. Program., 2003)

Free theorems in the presence of seq. - Patricia Johann; Janis Voigtländer (POPL, 2004)

Monadic augment and generalised short cut fusion. - Neil Ghani; Patricia Johann; Tarmo Uustalu; Varmo Vene (ICFP, 2005)

On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi. - Patricia Johann (Math. Struct. Comput. Sci., 2005)

The Impact of seq on Free Theorems-Based Program Transformations. - Patricia Johann; Janis Voigtländer (Fundam. Informaticae, 2006)

Initial Algebra Semantics Is Enough! - Patricia Johann; Neil Ghani (TLCA, 2007)

Monadic augment and generalised short cut fusion. - Neil Ghani; Patricia Johann (J. Funct. Program., 2007)

Selective strictness and parametricity in structural operational semantics, inequationally. - Janis Voigtländer; Patricia Johann (Theor. Comput. Sci., 2007)

Foundations for structured programming with GADTs. - Patricia Johann; Neil Ghani (POPL, 2008)

Short Cut Fusion for Effects. - Neil Ghani; Patricia Johann (Trends in Functional Programming, 2008)

A family of syntactic logical relations for the semantics of Haskell-like languages. - Patricia Johann; Janis Voigtländer (Inf. Comput., 2009)

A principled approach to programming with nested types in Haskell. - Patricia Johann; Neil Ghani (High. Order Symb. Comput., 2009)

Fibrational Induction Rules for Initial Algebras. - Neil Ghani; Patricia Johann; Clément Fumex (CSL, 2010)

A Generic Operational Metatheory for Algebraic Effects. - Patricia Johann; Alex Simpson; Janis Voigtländer (LICS, 2010)

When Is a Type Refinement an Inductive Type? - Robert Atkey; Patricia Johann; Neil Ghani (FoSSaCS, 2011)

Fibrational Induction Meets Effects. - Robert Atkey; Neil Ghani; Bart Jacobs 001; Patricia Johann (FoSSaCS, 2012)

Refining Inductive Types - Robert Atkey; Patricia Johann; Neil Ghani (Log. Methods Comput. Sci., 2012)

Generic Fibrational Induction - Neil Ghani; Patricia Johann; Clément Fumex (Log. Methods Comput. Sci., 2012)

Abstraction and invariance for algebraically indexed types. - Robert Atkey; Patricia Johann; Andrew Kennedy (POPL, 2013)

Indexed Induction and Coinduction, Fibrationally. - Neil Ghani; Patricia Johann; Clément Fumex (Log. Methods Comput. Sci., 2013)

A relationally parametric model of dependent type theory. - Robert Atkey; Neil Ghani; Patricia Johann (POPL, 2014)

Structural Resolution for Logic Programming. - Patricia Johann; Ekaterina Komendantskaya; Vladimir Komendantskiy (ICLP (Technical Communications), 2015)

Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic. - Ekaterina Komendantskaya; Patricia Johann (CoRR, 2015)

Bifibrational Functorial Semantics of Parametric Polymorphism. - Neil Ghani; Patricia Johann; Fredrik Nordvall Forsberg; Federico Orsanigo; Tim Revell (MFPS, 2015)

Interleaving data and effects. - Robert Atkey; Patricia Johann (J. Funct. Program., 2015)

A Productivity Checker for Logic Programming. - Ekaterina Komendantskaya; Patricia Johann; Martin Schmidt 002 (LOPSTR, 2016)

Cubical Categories for Higher-Dimensional Parametricity. - Patricia Johann; Kristina Sojakova (CoRR, 2017)

A General Framework for Relational Parametricity. - Kristina Sojakova; Patricia Johann (LICS, 2018)

On local presentability of T/A. - Patricia Johann; Andrew Polonsky (CoRR, 2018)

Higher-Kinded Data Types: Syntax and Semantics. - Patricia Johann; Andrew Polonsky (LICS, 2019)

Deep Induction: Induction Rules for (Truly) Nested Types. - Patricia Johann; Andrew Polonsky (FoSSaCS, 2020)

Preface. - Patricia Johann (MFPS, 2020)

Local Presentability of Certain Comma Categories. - Andrew Polonsky; Patricia Johann (Appl. Categorical Struct., 2020)

Parametricity for Primitive Nested Types. - Patricia Johann; Enrico Ghiorzi; Daniel Jeffries (FoSSaCS, 2021)

Parametricity for Nested Types and GADTs. - Patricia Johann; Enrico Ghiorzi; Daniel Jeffries (CoRR, 2021)

GADTs, Functoriality, Parametricity: Pick Two. - Patricia Johann; Enrico Ghiorzi; Daniel Jeffries (LSFA, 2021)

(Deep) Induction Rules for GADTs. - Patricia Johann; Enrico Ghiorzi; Daniel Jeffries (CoRR, 2021)

Parametricity for Nested Types and GADTs. - Patricia Johann; Enrico Ghiorzi (Log. Methods Comput. Sci., 2021)

Characterizing Functions Mappable over GADTs. - Patricia Johann; Pierre Cagne (APLAS, 2022)

(Deep) induction rules for GADTs. - Patricia Johann; Enrico Ghiorzi (CPP, 2022)

How Functorial Are (Deep) GADTs? - Patricia Johann; Pierre Cagne (CoRR, 2022)

Early Announcement: Parametricity for GADTs. - Pierre Cagne; Patricia Johann (CoRR, 2024)

GADTs are not (Even partial) functors. - Pierre Cagne; Enrico Ghiorzi; Patricia Johann (Math. Struct. Comput. Sci., 2024)

Deep Induction for Inductive Families. - Patricia Johann; Edward Morehouse (WoLLIC, 2025)