Publications
[29] Programming with Nested Types: A Principled Approach. Patricia Johann and Neil Ghani. Submitted, 2007.
[28] Short Cut Fusion of Recursive Programs with Computational Effects. Neil Ghani and Patricia Johann. Accepted for presentation at the Symposium on Trends in Functional Programming 2008 (TFP'08). [pdf]
[27] Using Kan Extensions to Structure and Reason About Functional Programs. Neil Ghani and Patricia Johann. Accepted, Journal of Functional Programming.
[26] A Family of Syntactic Logical Relations for the Semantics of Haskell. Patricia Johann and Janis Voigtlaender. Accepted, Information and Computation. [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 [21].) [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.