publications: - title: "Monadic augment and generalised short cut fusion" author: - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Tarmo Uustalu" link: "http://www.ioc.ee/~tarmo/" - name: "Varmo Vene" link: "https://researchr.org/alias/varmo-vene" year: "2005" doi: "http://doi.acm.org/10.1145/1086365.1086403" links: doi: "http://doi.acm.org/10.1145/1086365.1086403" researchr: "https://researchr.org/publication/GhaniJUV05" cites: 0 citedby: 0 pages: "294-305" booktitle: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005" editor: - name: "Olivier Danvy" link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/" - name: "Benjamin C. Pierce" link: "http://www.cis.upenn.edu/~bcpierce/" publisher: "ACM" isbn: "1-59593-064-7" kind: "inproceedings" key: "GhaniJUV05" - title: "Foundations for structured programming with GADTs" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" year: "2008" doi: "http://doi.acm.org/10.1145/1328438.1328475" links: doi: "http://doi.acm.org/10.1145/1328438.1328475" tags: - "programming" researchr: "https://researchr.org/publication/JohannG08" cites: 0 citedby: 0 pages: "297-308" booktitle: "Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008" editor: - name: "George C. Necula" link: "https://researchr.org/alias/george-c.-necula" - name: "Philip Wadler" link: "http://homepages.inf.ed.ac.uk/wadler/" publisher: "ACM" isbn: "978-1-59593-689-9" kind: "inproceedings" key: "JohannG08" - title: "An Improved General E-Unification Method" author: - name: "Daniel J. Dougherty" link: "https://researchr.org/alias/daniel-j.-dougherty" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1992" tags: - "e-science" researchr: "https://researchr.org/publication/DoughertyJ92%3A0" cites: 0 citedby: 0 journal: "Journal of Symbolic Computation" volume: "14" number: "4" pages: "303-320" kind: "article" key: "DoughertyJ92:0" - title: "Fibrational Induction Rules for Initial Algebras" author: - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Clément Fumex" link: "https://researchr.org/alias/cl%C3%A9ment-fumex" year: "2010" doi: "http://dx.doi.org/10.1007/978-3-642-15205-4_27" links: doi: "http://dx.doi.org/10.1007/978-3-642-15205-4_27" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/csl/GhaniJF10" tags: - "rule-based" - "rules" - " algebra" researchr: "https://researchr.org/publication/GhaniJF10" cites: 0 citedby: 0 pages: "336-350" booktitle: "Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings" editor: - name: "Anuj Dawar" link: "https://researchr.org/alias/anuj-dawar" - name: "Helmut Veith" link: "https://researchr.org/alias/helmut-veith" volume: "6247" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-642-15204-7" kind: "inproceedings" key: "GhaniJF10" - title: "A Generalization of Short-Cut Fusion and its Correctness Proof" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2002" researchr: "https://researchr.org/publication/Johann02%3A0" cites: 0 citedby: 0 journal: "Higher-Order and Symbolic Computation" volume: "15" number: "4" pages: "273-300" kind: "article" key: "Johann02:0" - title: "Free theorems in the presence of seq" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2004" doi: "http://doi.acm.org/10.1145/964001.964010" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, the standard parametricity theorem fails for nonstrict languages supporting a polymorphic strict evaluation primitive like Haskell's seq. Contrary to the folklore surrounding seq and parametricity, we show that not even quantifying only over strict and bottom-reflecting relations in the forall-clause of the underlying logical relation --- and thus restricting the choice of functions with which such relations are instantiated to obtain free theorems to strict and total ones --- is sufficient to recover from this failure. By addressing the subtle issues that arise when propagating up the type hierarchy restrictions imposed on a logical relation in order to accommodate the strictness primitive, we provide a parametricity theorem for the subset of Haskell corresponding to a Girard-Reynolds-style calculus with fixpoints, algebraic datatypes, and seq. A crucial ingredient of our approach is the use of an asymmetric logical relation, which leads to ``inequational'' versions of free theorems enriched by preconditions guaranteeing their validity in the described setting. Besides the potential to obtain corresponding preconditions for standard equational free theorems by combining some new inequational ones, the latter also have value in their own right, as is exemplified with a careful analysis of seq's impact on familiar program transformations." links: doi: "http://doi.acm.org/10.1145/964001.964010" successor: "https://researchr.org/publication/JV06" tags: - "programming languages" - "program analysis" - "transformation language" - "functional programming" - "analysis" - "Haskell" - " algebra" - "higher-order transformations" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/JV04" cites: 0 citedby: 0 pages: "99-110" booktitle: "Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004" editor: - name: "Neil D. Jones" link: "http://www.diku.dk/hjemmesider/ansatte/neil/" - name: "Xavier Leroy" link: "http://pauillac.inria.fr/~xleroy/" publisher: "ACM" isbn: "1-58113-729-X" kind: "inproceedings" key: "JV04" - title: "The Impact of seq on Free Theorems-Based Program Transformations" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2006" doi: "http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=69&issue=1&spage=63" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results --- including so-called free theorems --- fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq." links: doi: "http://iospress.metapress.com/openurl.asp?genre=article&issn=0169-2968&volume=69&issue=1&spage=63" tags: - "programming languages" - "rule-based" - "transformation language" - "functional programming" - "Haskell" - " algebra" - "systematic-approach" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/JV06" cites: 0 citedby: 0 journal: "Fundamenta Informaticae" volume: "69" number: "1-2" pages: "63-102" kind: "article" key: "JV06" - title: "Selective strictness and parametricity in structural operational semantics, inequationally" author: - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2007" doi: "http://dx.doi.org/10.1016/j.tcs.2007.09.014" abstract: "Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. The formal background of such `free theorems' is well developed for extensions of the Girard-Reynolds polymorphic lambda calculus by algebraic datatypes and general recursion, provided the resulting calculus is endowed with either a purely strict or a purely nonstrict semantics. But modern functional languages like Clean and Haskell, while using nonstrict evaluation by default, also provide means to enforce strict evaluation of subcomputations at will. The resulting selective strictness gives the advanced programmer explicit control over evaluation order, but is not without semantic consequences: it breaks standard parametricity results. This paper develops an operational semantics for a core calculus supporting all the language features emphasized above. Its main achievement is the characterization of observational approximation with respect to this operational semantics via a carefully constructed logical relation. This establishes the formal basis for new parametricity results, as illustrated by several example applications, including the first complete correctness proof for short cut fusion in the presence of selective strictness. The focus on observational approximation, rather than equivalence, allows a finer-grained analysis of computational behavior in the presence of selective strictness than would be possible with observational equivalence alone." links: doi: "http://dx.doi.org/10.1016/j.tcs.2007.09.014" tags: - "programming languages" - "semantics" - "program analysis" - "completeness" - "formal semantics" - " structural operational semantics" - "functional programming" - "analysis" - "Haskell" - " algebra" - "operational semantics" researchr: "https://researchr.org/publication/VJ07%3A1" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "388" number: "1-3" pages: "290-318" kind: "article" key: "VJ07:1" - title: "A Generic Operational Metatheory for Algebraic Effects" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Alex Simpson" link: "http://homepages.inf.ed.ac.uk/als/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2010" doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2010.29" abstract: "We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of algebraic effects, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power’s structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive “basic preorder” on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity." links: doi: "http://doi.ieeecomputersociety.org/10.1109/LICS.2010.29" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/JohannSV10" tags: - "programming languages" - "semantics" - "program analysis" - "generic programming" - " structural operational semantics" - "relational algebra" - "analysis" - "metatheory" - " algebra" - "programming" - "operational semantics" - "context-aware" - "systematic-approach" researchr: "https://researchr.org/publication/JSV10" cites: 0 citedby: 0 pages: "209-218" booktitle: "Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom" publisher: "IEEE Computer Society" isbn: "978-0-7695-4114-3" kind: "inproceedings" key: "JSV10" - title: "Short Cut Fusion: Proved and Improved" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2001" doi: "http://link.springer.de/link/service/series/0558/bibs/2196/21960047.htm" links: doi: "http://link.springer.de/link/service/series/0558/bibs/2196/21960047.htm" researchr: "https://researchr.org/publication/Johann01" cites: 0 citedby: 0 pages: "47-71" booktitle: "Semantics, Applications, and Implementation of Program Generation, Second International Workshop, SAIG 2001, Florence, Italy, September 6, 2001, Proceedings" editor: - name: "Walid Taha" link: "http://www.cs.rice.edu/~taha/" volume: "2196" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-42558-6" kind: "inproceedings" key: "Johann01" - title: "Initial Algebra Semantics Is Enough!" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" year: "2007" doi: "http://dx.doi.org/10.1007/978-3-540-73228-0_16" links: doi: "http://dx.doi.org/10.1007/978-3-540-73228-0_16" tags: - "semantics" - " algebra" researchr: "https://researchr.org/publication/JohannG07" cites: 0 citedby: 0 pages: "207-222" booktitle: "Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings" editor: - name: "Simona Ronchi Della Rocca" link: "http://www.di.unito.it/~ronchi/" volume: "4583" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-540-73227-3" kind: "inproceedings" key: "JohannG07" - title: "A Combinatory Logic Approach to Higher-Order E-Unification" author: - name: "Daniel J. Dougherty" link: "https://researchr.org/alias/daniel-j.-dougherty" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1995" doi: "http://dx.doi.org/10.1016/0304-3975(94)00210-A" links: doi: "http://dx.doi.org/10.1016/0304-3975(94)00210-A" tags: - "e-science" - "logic" - "systematic-approach" researchr: "https://researchr.org/publication/DoughertyJ95" cites: 0 citedby: 0 journal: "Theoretical Computer Science" volume: "139" number: "1&2" pages: "207-242" kind: "article" key: "DoughertyJ95" - title: "Short cut fusion is correct" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2003" doi: "http://dx.doi.org/10.1017/S0956796802004409" links: doi: "http://dx.doi.org/10.1017/S0956796802004409" researchr: "https://researchr.org/publication/Johann03" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "13" number: "4" pages: "797-814" kind: "article" key: "Johann03" - title: "A family of syntactic logical relations for the semantics of Haskell-like languages" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Janis Voigtländer" link: "http://www.iai.uni-bonn.de/~jv/" year: "2009" doi: "http://dx.doi.org/10.1016/j.ic.2007.11.009" abstract: "Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations." links: doi: "http://dx.doi.org/10.1016/j.ic.2007.11.009" tags: - "laziness" - "programming languages" - "semantics" - "rule-based" - "program analysis" - "pattern language" - "functional programming" - "analysis" - "Haskell" - "pattern matching" - "programming" researchr: "https://researchr.org/publication/JV09" cites: 0 citedby: 0 journal: "Inf. Comput." volume: "207" number: "2" pages: "341-368" kind: "article" key: "JV09" - title: "A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract)" author: - name: "Daniel J. Dougherty" link: "https://researchr.org/alias/daniel-j.-dougherty" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1992" tags: - "e-science" - "logic" - "systematic-approach" researchr: "https://researchr.org/publication/DoughertyJ92" cites: 0 citedby: 0 pages: "79-93" booktitle: "Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings" editor: - name: "Deepak Kapur" link: "https://researchr.org/alias/deepak-kapur" volume: "607" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-55602-8" kind: "inproceedings" key: "DoughertyJ92" - title: "Warm fusion in Stratego: A case study in generation of program transformation systems" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2000" doi: "http://dx.doi.org/10.1023/A:1018956702672" abstract: "Stratego is a domain-specific language for the specification of program transformation systems. The design of Stratego is based on the paradigm of rewriting strategies: user-definable programs in a little language of strategy operators determine where and in what order transformation rules are (automatically) applied to a program. The separation of rules and strategies supports modularity of specifications. Stratego also provides generic features for specification of program traversals. In this paper we present a case study of Stratego as applied to a non-trivial problem in program transformation. We demonstrate the use of Stratego in eliminating intermediate data structures from (also known as deforesting) functional programs via the warm fusion algorithm of Launchbury and Sheard. This algorithm has been specified in Stratego and embedded in a fully automatic transformation system for kernel Haskell. The entire system consists of about 2600 lines of specification code, which breaks down into 1850 lines for a general framework for Haskell transformation and 750 lines devoted to a highly modular, easily extensible specification of the warm fusion transformer itself. Its successful design and construction provides further evidence that programs generated from Stratego specifications are suitable for integration into real systems, and that rewriting strategies are a good paradigm for the implementation of such systems. " links: doi: "http://dx.doi.org/10.1023/A:1018956702672" "stratego wiki": "http://www.program-transformation.org/Stratego/WarmFusionInStratego" tags: - "programming languages" - "optimization" - "rule-based" - "data-flow language" - "generic programming" - "case study" - "graph transformation" - "Stratego/XT" - "traversal" - "deforestation" - "transformation language" - "functional programming" - "language design" - "Haskell" - "data-flow programming" - "little language" - "data-flow" - "graph-rewriting" - "rules" - "programming paradigms" - "code generation" - "warm fusion" - "transformation system" - "programming" - "program optimization" - "higher-order transformations" - "rewriting" - "design" - "extensible language" - "rewriting strategies" - "transformation" - "Stratego" - "program transformation" - "domain-specific language" researchr: "https://researchr.org/publication/JohannV00" cites: 1 citedby: 0 journal: "Annals of Mathematics and Artificial Intelligence" volume: "29" number: "1-4" pages: "1-34" kind: "article" key: "JohannV00" - title: "Fusing Logic and Control with Local Transformations: An Example Optimization" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2001" doi: "https://doi.org/10.1016/S1571-0661(04)00271-3" abstract: "Abstract programming supports the separation of logical concerns from issues of control in program construction. While this separation of concerns leads to reduced code size and increased reusability of code, its main disadvantage is the computa- tional overhead it incurs. Fusion techniques can be used to combine the reusability of abstract programs with the efficiency of specialized programs. In this paper we illustrate some of the ways in which rewriting strategies can be used to separate the definition of program transformation rules from the strategies under which they are applied. Doing so supports the generic definition of program transformation components. Fusion techniques for strategies can then be used to specialize such generic components. We show how the generic innermost rewriting strategy can be optimized by fusing it with the rules to which it is applied. Both the optimization and the programs to which the optimization applies are specified in the strategy language Stratego. The optimization is based on small transformation rules that are applied locally under the control of strategies, using special knowledge about the contexts in which the rules are applied. " links: doi: "https://doi.org/10.1016/S1571-0661(04)00271-3" tags: - "programming languages" - "optimization" - "reusable components" - "rule-based" - "generic programming" - "graph transformation" - "separation of concerns" - "Stratego/XT" - "transformation language" - "term rewriting" - "reuse" - "graph-rewriting" - "rules" - "logic programming" - "programming" - "context-aware" - "logic" - "program optimization" - "innermost rewriting" - "rewriting logic" - "rewriting" - "rewriting strategies" - "transformation" - "Stratego" - "program transformation" researchr: "https://researchr.org/publication/JohannV01" cites: 0 citedby: 0 journal: "Electronic Notes in Theoretical Computer Science" volume: "57" pages: "144-162" kind: "article" key: "JohannV01" - title: "Solving Simplification Ordering Constraints" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Rolf Socher-Ambrosius" link: "https://researchr.org/alias/rolf-socher-ambrosius" year: "1994" tags: - "constraints" researchr: "https://researchr.org/publication/JohannS94" cites: 0 citedby: 0 pages: "352-367" booktitle: "Constraints in Computational Logics, First International Conference, CCL 94, Munich, Germant, September 7-9, 1994" editor: - name: "Jean-Pierre Jouannaud" link: "https://researchr.org/alias/jean-pierre-jouannaud" volume: "845" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-58403-X" kind: "inproceedings" key: "JohannS94" - title: "A principled approach to programming with nested types in Haskell" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" year: "2009" doi: "http://dx.doi.org/10.1007/s10990-009-9047-7" links: doi: "http://dx.doi.org/10.1007/s10990-009-9047-7" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/lisp/JohannG09" tags: - "Haskell" - "programming" - "systematic-approach" researchr: "https://researchr.org/publication/JohannG09" cites: 0 citedby: 0 journal: "Higher-Order and Symbolic Computation" volume: "22" number: "2" pages: "155-189" kind: "article" key: "JohannG09" - title: "Monadic augment and generalised short cut fusion" author: - name: "Neil Ghani" link: "http://personal.cis.strath.ac.uk/~ng/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2007" doi: "http://dx.doi.org/10.1017/S0956796807006314" links: doi: "http://dx.doi.org/10.1017/S0956796807006314" researchr: "https://researchr.org/publication/GhaniJ07" cites: 0 citedby: 0 journal: "Journal of Functional Programming" volume: "17" number: "6" pages: "731-776" kind: "article" key: "GhaniJ07" - title: "An Improved General E-Unification Method" author: - name: "Daniel J. Dougherty" link: "https://researchr.org/alias/daniel-j.-dougherty" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1990" tags: - "e-science" researchr: "https://researchr.org/publication/DoughertyJ90" cites: 0 citedby: 0 pages: "261-275" booktitle: "10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings" editor: - name: "Mark E. Stickel" link: "https://researchr.org/alias/mark-e.-stickel" volume: "449" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-52885-7" kind: "inproceedings" key: "DoughertyJ90" - title: "Normal Forms in Combinatory Logic" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1994" tags: - "logic" researchr: "https://researchr.org/publication/Johann94" cites: 0 citedby: 0 journal: "Notre Dame Journal of Formal Logic" volume: "35" number: "4" pages: "573-594" kind: "article" key: "Johann94" - title: "On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2005" doi: "http://dx.doi.org/10.1017/S0960129504004578" links: doi: "http://dx.doi.org/10.1017/S0960129504004578" tags: - "rule-based" - "higher-order transformations" - "transformation" - "program transformation" researchr: "https://researchr.org/publication/Johann05" cites: 0 citedby: 0 journal: "Mathematical Structures in Computer Science" volume: "15" number: "2" pages: "201-229" kind: "article" key: "Johann05" - title: "Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" - name: "Michael Kohlhase" link: "https://researchr.org/alias/michael-kohlhase" year: "1994" researchr: "https://researchr.org/publication/JohannK94" cites: 0 citedby: 0 pages: "620-634" booktitle: "Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings" editor: - name: "Alan Bundy" link: "https://researchr.org/alias/alan-bundy" volume: "814" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-58156-1" kind: "inproceedings" key: "JohannK94" - title: "A funny thing happened on the way to the formula: demonstrating equality of functions and programs" author: - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "1999" doi: "http://doi.acm.org/10.1145/349522.349387" links: doi: "http://doi.acm.org/10.1145/349522.349387" researchr: "https://researchr.org/publication/Johann99" cites: 0 citedby: 0 journal: "ACM SIGCSE Bulletin" volume: "31" number: "4" pages: "32-34" kind: "article" key: "Johann99" - title: "Staged Notational Definitions" author: - name: "Walid Taha" link: "http://www.cs.rice.edu/~taha/" - name: "Patricia Johann" link: "http://personal.cis.strath.ac.uk/~patricia/" year: "2003" doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2830&spage=97" links: doi: "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2830&spage=97" researchr: "https://researchr.org/publication/TahaJ03" cites: 0 citedby: 0 pages: "97-116" booktitle: "Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings" editor: - name: "Frank Pfenning" link: "http://www.cs.cmu.edu/~fp/" - name: "Yannis Smaragdakis" link: "http://smaragd.org" volume: "2830" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "3-540-20102-5" kind: "inproceedings" key: "TahaJ03"