@inproceedings{ASvvP:05,
  author = {A. Alimarine, S. Smetsers, A. van Weelden, M. van Eekelen and R. Plasmeijer},
  title = {There and back again: arrows for invertible programming},
  booktitle = {Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell},
  publisher = {ACM Press},
  year = {2005},
  pages = {86--97},
  note = {http://doi.acm.org/10.1145/1088348.1088357Electronic Edition},
  doi = {http://doi.acm.org/10.1145/1088348.1088357}
}

@article{SA:93,
  author = {S. Abramsky},
  title = {Computational Interpretations of Linear Logic},
  journal = {Theoretical Computer Science},
  year = {1993},
  volume = {111},
  number = {1-2},
  pages = {3--57}
}

@inproceedings{AASSAvW:05,
  author = {Artem Alimarine and Sjaak Smetsers and Arjen van Weelden and Marko C. J. D. van Eekelen and Rinus Plasmeijer},
  title = {There and back again: arrows for invertible programming},
  booktitle = {Haskell},
  publisher = {ACM},
  year = {2005},
  pages = {86--97},
  url = {http://doi.acm.org/10.1145/1088348.1088357}
}

@book{BO:97,
  author = {R. S. Bird and O. De Moor},
  title = {Algebra of Programming},
  publisher = {Prentice-Hall International Series in Computer Science},
  year = {1997},
  volume = {100},
  note = { http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/Project's Webpage},
  url = {http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/}
}

@inproceedings{BD:74,
  author = {C. Böhm and M. Dezani-Ciancaglini},
  title = {Combinatorial Problems, Combinator Equations and Normal Forms},
  booktitle = {Proceedings of the 2nd Colloquium on Automata, Languages and Programming},
  journal = {Automata, Languages and Programming, Second Colloquium, Saarbrücken},
  publisher = {Lecture Notes in Computer Science, Springer-Verlag},
  year = {1974},
  volume = {14},
  pages = {185--199},
  note = {http://portal.acm.org/citation.cfm?id=646230.681874Electronic Edition}
}

@techreport{CP:02,
  author = {J. Cai and R. Paige},
  title = {Multiset Discrimination - A Method for Implementing Programming Language Systems without Hashing},
  year = {1992},
  number = {TR1992-609},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.5597Electronic Edition}
}

@inproceedings{FM:94,
  author = {A. Felty and D. Howe},
  title = {Generalization and Reuse of Tactic Proofs},
  booktitle = {5th International Conference on Logic Programming and Automated Reasoning},
  publisher = {Springer-Verlag },
  year = {1994},
  volume = {822},
  pages = {1--15},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1064Electronic Edition}
}

@article{JG:00,
  author = {Jeremy Gibbons},
  title = {Generic downwards accumulations},
  journal = {Science of Computer Programming},
  year = {2000},
  volume = {37},
  number = {1-3},
  pages = {37 --65}
}

@article{Gil:01,
  author = {J. Gil},
  title = {Subtyping arithmetical types.},
  booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  journal = {SIGPLAN},
  publisher = {ACM Press},
  year = {2001},
  volume = {36},
  number = {3},
  pages = {276-289},
  note = {http://doi.acm.org/10.1145/360204.360232Electronic Edition},
  doi = {http://doi.acm.org/10.1145/373243.360232}
}

@inproceedings{RHCG:93,
  author = {Rachel Harrison and Celia A. Glass},
  title = {Dynamic Programming in a Pure Functional Language},
  booktitle = {Proceedings of the ACM/SIGAPP Symposium on Applied
 Computing},
  year = {1993},
  pages = {179--186},
  url = {http://doi.acm.org/10.1145/162754.162864}
}

@article{Hug:89,
  author = {R. J. M. Hughes},
  title = {Why Functional Programming Matters},
  journal = {The Computer Journal},
  year = {1989},
  volume = {32},
  number = {2},
  pages = {98--107},
  note = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.htmlElectronic Edition},
  url = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.html}
}

@article{JG:95,
  author = {C. B. Jay and N. Ghani},
  title = {The Virtues of Eta-expansion},
  journal = {Journal of Functional Programming},
  year = {1995},
  volume = {5},
  number = {2},
  pages = {135--154},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.613Electronic Edition}
}

@inproceedings{SlP:96,
  author = {Simon L. Peyton Jones},
  title = {Compiling Haskell by Program Transformation: A Report from the Trenches},
  booktitle = {Programming Languages and Systems---ESOP'96},
  publisher = {Springer-Verlag},
  year = {1996},
  volume = {1058},
  pages = {18--44}
}

@article{SPJAS:98,
  author = {Simon L. Peyton Jones and André L. M. Santos},
  title = {A transformation-based optimiser for~Haskell},
  journal = {Science of Computer Programming},
  year = {1998},
  volume = {32},
  number = {1--3},
  pages = {3--47}
}

@article{MM:82,
  author = {A. Martelli and U. Montanari},
  title = {An Efficient Unification Algorithm},
  journal = {AMC Transactions on Programming Languages and Systems},
  publisher = {Association of Computing Machinery Press},
  year = {1982},
  volume = {4},
  number = {2},
  pages = {258--282},
  note = {http://doi.acm.org/10.1145/357162.357169Electronic Edition},
  doi = {http://doi.acm.org/10.1145/357162.357169}
}

@inproceedings{DM:91b,
  author = {D. Miller},
  title = {Unification of Simply Typed Lambda-Terms as Logic Programming},
  booktitle = {Proc. Int. Conference on Logic Programming (Paris)},
  publisher = {MIT Press},
  year = {1991},
  pages = {255--269}
}

@article{Mil:91,
  author = {D. Miller},
  title = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification},
  journal = {Journal of Logic and Computation},
  year = {1991},
  volume = {1},
  pages = {253 -- 281},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.8958Electronic Edition }
}

@article{DM:91a,
  author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
  title = {Uniform Proofs as a Foundation for Logic Programming},
  journal = {Annals of Pure and Applied Logic},
  year = {1991},
  volume = {51},
  number = {1--2},
  pages = {125--157}
}

@misc{SMND:97,
  author = {Subrata Mitra and Nachum Dershowitz},
  title = {Matching and Unification in Rewrite Theories},
  year = {1997},
  url = {http://citeseer.ist.psu.edu/52607.html}
}

@incollection{AP:98,
  author = {Alberto Pardo},
  title = {Fusion of Monadic (Co)Recursive Programs},
  booktitle = {Informal Proc. of Wksh. on Generic Programming (WGP'98, Marstrand, Sweden, 18 June 1998)},
  publisher = {Dept. of Computing Science, Chalmers Univ. of Techn., and Göteborg Univ.},
  year = {1998},
  note = {Electronic version available at http://wsinwp01.win.tue.nl:1234/WGPProceedings/},
  url = {http://www.fing.edu.uy/~pardo/papers/wgp98.ps.gz}
}

@inproceedings{FPCE:88,
  author = {Frank Pfenning and Conal Elliot},
  title = {Higher-Order Abstract Syntax},
  booktitle = {Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI)},
  year = {1988},
  pages = {199--208}
}

@misc{BP:96,
  author = {Benjamin C. Pierce},
  title = {Foundational Calculi for Programming Languages},
  year = {1996},
  url = {http://citeseer.ist.psu.edu/55202.html; http://www.cs.indiana.edu/ftp/pierce/crchandbook.ps.gz}
}

@phdthesis{Pre:95,
  author = {C. Prehofer},
  title = {Solving Higher-Order Equations: From Logic to Programming},
  school = {Technische Universität München},
  year = {1995},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.3626Electronic Edition}
}

@article{Rit:91,
  author = {M. Rittri},
  title = {Using types as search keys in function libraries},
  journal = {Journal of Functional Programming},
  year = {1991},
  volume = {1},
  number = {1},
  pages = {71--89},
  note = {http://dx.doi.org/10.1145/99370.99384Electronic Edition},
  url = {http://dx.doi.org/10.1145/99370.99384}
}

@inproceedings{RW:91,
  author = {E. Rollins and J. Wing},
  title = {Specifications as Search Keys for Software Libraries},
  booktitle = {8th International Conference on Logic Programming},
  publisher = {MIT press},
  year = {1991},
  pages = {173--187},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.8746Electronic Edition}
}

@article{RT:91,
  author = {C. Runciman and I. Toyn},
  title = {Retrieving Reusable Software Components by Polymorphic Type},
  journal = {Journal of Functional Programming},
  year = {1991},
  volume = {1},
  number = {2},
  pages = {191--211},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6545Electronic Edition}
}

@other{HASKELL,
  author = {S. P. Lones, P. Walder},
  title = {Haskell: A purely functional programming language},
  year = {1990},
  note = { http://www.haskell.org/Website}
}

@inproceedings{Sol:93,
  author = {S. Soloviev},
  title = {A Complete Axiom System for Isomorphism of Types in Closed Categories},
  booktitle = {LPAR '93: Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning},
  publisher = {Springer-Verlag},
  year = {1993},
  volume = {698},
  pages = {360--371},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.1383Electronic Edition}
}

@inproceedings{GS:94,
  author = {Guy L. Steele},
  title = {Building Interpreters by Composing Monads},
  booktitle = {Principles of Programming Languages},
  year = {1994},
  url = {http://www-swiss.ai.mit.edu/ftpdir/users/dae/related-papers/steele.ps.Z}
}

@inproceedings{ST:04,
  author = {Simon Thompson},
  title = {Refactoring Functional Programs},
  booktitle = {Advanced Functional Programming},
  year = {2004},
  pages = {331-357},
  doi = {http://dx.doi.org/10.1007/11546382_9}
}

@inproceedings{ST:89,
  author = {S. Thompson},
  title = {Functional Programming: Executable Specifications and Program Transformation},
  booktitle = {Proceedings of the 5th International Workshop on Software Specification and Design},
  publisher = {IEEE Computer Society Press},
  year = {1989},
  pages = {287--290}
}

@incollection{PW:94,
  author = {Philip Wadler},
  title = {Monads for functional programming},
  booktitle = {Program Design Calculi},
  publisher = {Springer Verlag},
  year = {1994},
  volume = {118},
  note = {Proceedings of the International Summer School at Marktoberdorf directed by F. L. Bauer, M. Broy, E. W. Dijkstra, D. Gries, and C. A. R. Hoare}
}

@inproceedings{Wad:89,
  author = {P. Wadler},
  title = {Theorems for Free},
  booktitle = {4th International Conference on Functional Programming Languages and Computer Architecture'89.},
  publisher = {ACM Press},
  year = {1989},
  pages = {347--359},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875Electronic Edition}
}

@incollection{PW:87,
  author = {Philip Wadler},
  title = {Views: A Way for Pattern Matching to Cohabit with Data Abstraction},
  booktitle = {Proceedings, 14th Symposium on Principles of Programming Languages},
  publisher = {Association for Computing Machinery},
  year = {1987},
  pages = {307--312}
}

@inproceedings{Wan:86,
  author = {M. Wand},
  title = {Finding the Source of Type Errors},
  booktitle = {Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {1986},
  pages = {38--43},
  note = {http://doi.acm.org/10.1145/512644.512648Electronic Edition},
  doi = {http://doi.acm.org/10.1145/512644.512648}
}

@inproceedings{XP:99,
  author = {H. Xi and F. Pfenning},
  title = {Dependent Types in Practical Programming},
  booktitle = {In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {1999},
  pages = {214--227},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.548Electronic Edition}
}

@inproceedings{ZGC:03,
  author = {Zibin and Gil and Considine},
  title = {Efficient Algorithms for Isomorphisms of Simple Types},
  booktitle = {30th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
  publisher = {ACM Press},
  year = {2003},
  pages = {160 - 171},
  note = {http://dx.doi.org/10.1017/S0960129505004913Electronic Edition},
  doi = {http://dx.doi.org/10.1017/S0960129505004913}
}