**Publications**

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

[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.

[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.