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

[54] Partiality Wrecks GADTs' Functoriality. Pierre Cagne and Patricia Johann. Accepted for presentation at 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.