**Publications**

[52] (Deep) Induction Rules for GADTs. Patricia Johann and Enrico Ghiorzi. To appear, Proceedings, Certified Programs and Proofs 2022 (CPP'22). [pdf] Accompanying code available here.

[51] Parametricity for Nested Types and GADTs. Patricia Johann and
Enrico Ghiorzi. Accepted for publication, *Logical Methods in
Computer Science*.

[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] Accompanying code available here.

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

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