[58] Deep Induction for Advanced Data Types. Patricia Johann and Ed Morehouse. Accepted for presentation at the Special Session on Proof Assistants at the May 2025 Meeting of the Association for Symbolic Logic.

[57] Parametricity for GADTs. Pierre Cagne and Patricia Johann. Proceedings, Mathematical Foundations of Program Semantics 2024 (MFPS'24). [pdf]

[56] GADTs Are Not (Even Partial) Functors. Pierre Cagne, Enrico Ghiorzi, and Patricia Johann. Mathematical Structures in Computer Science (2024), pp. 1-24, doi:10.1017/S0960129524000161. [pdf]

[55] GADTs are Not (Even Lax) Functors. Pierre Cagne and Patricia Johann. Structure Meets Power 2023 (SMP'23). [pdf]

[54] Partiality Wrecks GADTs' Functoriality. Pierre Cagne and Patricia Johann. Types for Proofs and Programs 2023 (TYPES'23). [pdf]

[53] Characterizing Functions Mappable Over GADTs. Patricia Johann and Pierre Cagne. Proceedings, Asian Symposium on Programming Languages and Systems 2022 (APLAS'22), pp. 135-154. [pdf] [verified artifact]

[52] (Deep) Induction Rules for GADTs. Patricia Johann and Enrico Ghiorzi. Proceedings, Certified Programs and Proofs 2022 (CPP'22), pp. 324-337. [pdf] [talk] [code]

[51] Parametricity for Nested Types and GADTs. Patricia Johann and Enrico Ghiorzi. Logical Methods in Computer Science 17(4), pp. 23:1-23:50, 2021. [pdf]

[50] GADTs, Functoriality, Parametricity: Pick Two. Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries. Proceedings, Logical and Semantic Frameworks with Applications (LSFA'21). [pdf] [talk]

[49] Parametricity for Primitive Nested Types. Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries. Proceedings, Foundations of Software Science and Computation Structures 2021 (FoSSaCS'21), pp. 324-343. [pdf] [talk]

[48] Deep Induction: Induction Rules for (Truly) Nested Types. Patricia Johann and Andrew Polonsky. Proceedings, Foundations of Software Science and Computation Structures 2020 (FoSSaCS'20), pp. 339-358. [pdf] [code]

[47] Local Presentability of Certain Comma Categories. Andrew Polonsky and Patricia Johann. Applied Categorical Structures 28(1) (2020), pp. 135-142. [pdf]

[46] Higher-Kinded Data Types: Syntax and Semantics. Patricia Johann and Andrew Polonsky. Proceedings, Logic in Computer Science 2019 (LICS'19). [pdf]

[45] A General Framework for Relational Parametricity. Kristina Sojakova and Patricia Johann. Proceedings, Logic in Computer Science 2018 (LICS'18), pp. 869-878. [pdf][talk] [technical report]

[44] A Productivity Checker for Logic Programming. Ekaterina Komendantskaya, Patricia Johann, and Martin Schmidt. Logic-Based Program Synthesis and Transformation 2016 (LOPSTR'16), pp. 168-186. [pdf] An extended version with appendices containing all proofs and pseudocode algorithms is available on the ArXiv.

[43] Interleaving Data and Effects. Robert Atkey and Patricia Johann. Journal of Functional Programming 25(e20), 2015. [pdf]

[42] Structural Resolution for Automated Verification. Ekaterina Komendantskaya, Peng Fu, and Patricia Johann. Automated Verification of Critical Systems 2015 (AVoCS'15). [pdf]

[41] Structural Resolution for Logic Programming. Patricia Johann, Ekaterina Komendantskaya, and Vladimir Komendantskiy. Technical Communications of International Conference on Logic Programming (ICLP'15). [pdf]

[40] Bifibrational Functorial Semantics for Parametric Polymorphism. Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell. Proceedings, Mathematical Foundations of Program Semantics 2015 (MFPS'15), pp. 165-181. [pdf]

[39] A Relationally Parametric Model of Dependent Type Theory. Robert Atkey, Neil Ghani, and Patricia Johann. Proceedings, Principles of Programming Languages 2014 (POPL'14), pp. 503-516. [pdf]

[38] Indexed Induction and Coinduction, Fibrationally. Neil Ghani, Patricia Johann, and Clement Fumex. Logical Methods in Computer Science 9(3:6), pp. 1-31, 2013. [pdf]

[37] Abstraction and Invariance for Algebraically Indexed Types. Robert Atkey, Patricia Johann, and Andrew Kennedy. Proceedings, Principles of Programming Languages 2013 (POPL'13), pp. 87-100. [pdf]

[36] Generic Fibrational Induction. Neil Ghani, Patricia Johann, and Clement Fumex. Logical Methods in Computer Science 8(2), 2012. [pdf]

[35] Refining Inductive Types. Robert Atkey, Patricia Johann, and Neil Ghani. Logical Methods in Computer Science 8(2), 2012. [pdf]

[34] Fibrational Induction Meets Effects. Robert Atkey, Neil Ghani, Bart Jacobs, and Patricia Johann. Proceedings, Foundations of Software Science and Computation Structures 2012 (FoSSaCS'12), pp. 42-57. [pdf]

[33] Indexed Induction and Coinduction, Fibrationally. Clement Fumex, Neil Ghani, and Patricia Johann. Proceedings, Conference on Algebra and Coalgebra on Computer Science 2011 (CALCO'11), pp. 176-191. [pdf]

[32] When is a Type Refinement an Inductive Type? Robert Atkey, Patricia Johann, and Neil Ghani. Proceedings, Foundations of Software Science and Computation Structures 2011 (FoSSaCS'11), pp. 72-87. [pdf]

[31] Fibrational Induction Rules for Initial Algebras. Neil Ghani, Patricia Johann, and Clement Fumex. Proceedings, Computer Science Logic 2010 (CSL'10), pp. 336-350. [pdf]

[30] A Generic Operational Metatheory for Algebraic Effects. Patricia Johann, Alex Simpson, and Janis Voigtlaender. Proceedings, Logic in Computer Science 2010 (LICS'10), pp. 209-218. [pdf]

[29] Haskell Programming with Nested Types: A Principled Approach. Patricia Johann and Neil Ghani. Higher-Order and Symbolic Computation, vol. 22, no. 2 (2010), pp. 155-189. [pdf]

[28] Monadic fold, Monadic build, Monadic Short Cut Fusion. Patricia Johann and Neil Ghani. Proceedings, Symposium on Trends in Functional Programming 2009 (TFP'09), pp. 9-23. [pdf]

[27] Short Cut Fusion of Recursive Programs with Computational Effects. Neil Ghani and Patricia Johann. Trends in Functional Programming, vol. 9 (2009), pp. 113-128. [pdf]

[26] A Family of Syntactic Logical Relations for the Semantics of Haskell. Patricia Johann and Janis Voigtlaender. Information and Computation, vol. 207, no. 2 (2009), pp. 341-368. [pdf]

[25] Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08), pp. 297-308. [pdf]

[24] Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally. Janis Voigtlaender and Patricia Johann. Theoretical Computer Science, vol. 388, no. 1-3 (2007), pp. 290-318. [pdf]

[23] Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani. Proceedings, Typed Lambda Calculus and Applications 2007 (TLCA'07), pp. 207-222. [pdf]

[22] Monadic Augment and Generalised Short Cut Fusion. Neil Ghani and Patricia Johann. Journal of Functional Programming, vol. 17, no. 6 (2007), pp. 731-776. (A significantly expanded version of [20].) [pdf]

[21] The Impact of seq on Free Theorems-Based Program Transformations. Patricia Johann and Janis Voigtlaender. Fundamenta Informaticae, Special Issue on Program Transformation, vol. 69, no. 1-2 (2006), pp. 63-102. [pdf]

[20] Monadic Augment and Generalised Short Cut Fusion. Neil Ghani, Patricia Johann, Tarmo Uustalu, and Varmo Vene. Proceedings, International Conference on Functional Programming 2005 (ICFP'05), pp. 294-305. [pdf]

[19] On Proving the Correctness of Program Transformations Based on Free Theorems for Higher-order Polymorphic Calculi. Patricia Johann. Mathematical Structures in Computer Science, vol. 15, no. 2 (2005), pp. 201-229. [pdf]

[18] Free Theorems in the Presence of seq. Patricia Johann and Janis Voigtlaender. Proceedings, Principles of Programming Languages 2004 (POPL'04), pp. 99-110. [pdf]

[17] Staged Notational Definitions. Walid Taha and Patricia Johann. Proceedings, Generative Programming and Component Engineering 2003 (GPCE'03), pp. 97-116. [pdf]

[16] Short Cut Fusion is Correct. Patricia Johann. Journal of Functional Programming, vol. 13, no. 4 (2003), pp. 797-814. [pdf]

[15] A Generalization of Short-Cut Fusion and Its Correctness Proof. Patricia Johann. Higher-Order and Symbolic Computation, vol. 15 (2002), pp. 273-300. [pdf]

[14] Lumberjack Summer Camp: A Cross-Institutional Undergraduate Research Experience in Computer Science. Patricia Johann and Franklyn Turbak. Computer Science Education, vol. 11, no. 4 (2001). [pdf]

[13] Short Cut Fusion: Proved and Improved. Patricia Johann. Proceedings, Workshop on the Semantics, Application, and Implementation of Program Generation (SAIG'01), Springer-Verlag LNCS 2196 (2001), pp. 47-71. [pdf]

[12] Fusing Logic and Control with Local Transformations: An Example Optimization. Patricia Johann and Eelco Visser. Proceedings, International Workshop on Reduction Strategies in Rewriting 2001 (WRS'01), pp. 129-146. Also appears in Electronic Notes in Theoretical Computer Science, vol. 57, 2001. [pdf]

[11] Warm Fusion in Stratego: A Case Study in Generation of Program Transformation Systems. Patricia Johann and Eelco Visser. Annals of Mathematics and Artificial Intelligence, vol. 29, no. 1-4 (2000), pp. 1-34. [pdf]

[10] A Funny Thing Happened on the Way to the Formula: Demonstrating Equality of Functions and Programs. Patricia Johann. SIGCSE Bulletin, vol. 34, no. 4 (1999), pp. 32-34.

[9] Deduction Systems. Rolf Socher-Ambrosius and Patricia Johann. Springer-Verlag, 1996.

[8] A Combinatory Logic Approach to Higher-order E-unification. Daniel J. Dougherty and Patricia Johann. Theoretical Computer Science B 139 (1995), pp. 207-242. [pdf]

[7] Normal Forms in Combinatory Logic. Patricia Johann. Notre Dame Journal of Formal Logic 35 (1994), pp. 573-594. [pdf]

[6] Solving Simplification Ordering Constraints. Patricia Johann and Rolf Socher-Ambrosius. Proceedings, Constraints in Computational Logic (CCL'94), Springer-Verlag LNCS 845 (1994), pp. 352-367. Also appears as Technical Report MPI-I-93-256, Max-Planck-Institut-für-Informatik (1993).

[5] A Combinator-based Order-sorted Higher-order Unification Algorithm. Patricia Johann. Presented at the Eighth International Workshop on Unification 1994 (UNIF'94). The full paper appears as Technical Report SR-93-16, Universität des Saarlandes (1993).

[4] Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading. Patricia Johann and Michael Kohlhase. Proceedings, International Conference on Automated Deduction (CADE'94), Springer-Verlag LNAI 814 (1994), pp. 620-634. The full paper appears as Technical Report SR-93-13, Universität des Saarlandes (1993). [pdf]

[3] An Improved General E-unification Method. Daniel J.Dougherty and Patricia Johann. Journal of Symbolic Computation 14 (1992), pp. 303-320. [pdf]

[2] A Combinatory Logic Approach to Higher-order E-unification (Extended abstract). Daniel J. Dougherty and Patricia Johann. Proceedings, Conference on Automated Deduction (CADE'92), Springer-Verlag LNAI 607 (1992), pp. 79-93.

[1] An Improved General E-unification Method. Daniel J. Dougherty and Patricia Johann. Proceedings, Conference on Automated Deduction (CADE'90), Springer-Verlag LNAI 449 (1990), pp. 261-275.