Publications



[45] Cubical Categories for Higher-Dimensional Parametricity. Patricia Johann and Kristina Sojakova. Submitted. Available on the ArXiv.

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

[BIO] | [HOME] | [TEACHING] | [BOOK] | [GRANTS]