refs.bib

@article{connelly-morris,
author = {Connelly, Richard and Morris, F Lockwood},
title = {A generalization of the trie data structure},
journal = {Mathematical structure in computer science},
volume = 5,
issue = 3,
year = 1995,
pages = {381-418}
}

@article{ttg,
author = {Najd, Shayan and Peyton Jones, Simon},
title = {Trees that grow},
year = {2017},
month = {January},
url = {https://www.microsoft.com/en-us/research/publication/trees-that-grow/},
pages = {47-62},
journal = {Journal of Universal Computer Science (JUCS)},
volume = {23},
chapter = {1},
}

@inproceedings{logict,
  abstract = {We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is easy in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive msplit. We present two implementations of the library: one using success and failure continuations; and the other using control operators for manipulating delimited continuations. Copyright {\textcopyright} 2005 ACM.},
  author = {Kiselyov, Oleg and Shan, Chung Chieh and Friedman, Daniel P. and Sabry, Amr},
  booktitle = {Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP},
  doi = {10.1145/1086365.1086390},
  isbn = {1595930647},
  keywords = {Continuations,Control delimiters,Haskell,Logic programming,Prolog,Streams},
  title = {{Backtracking, interleaving, and terminating Monad transformers (functional pearl)}},
  year = {2005}
}

@techreport{hamt,
  author = {Bagwell, Phil},
  title = {Ideal Hash Trees},
  year = {2001},
  month = {11},
  institution = {Infoscience Department, École Polytechnique Fédérale de Lausanne}
}

@article{adams,
  title={Functional Pearls Efficient sets—a balancing act},
  volume={3},
  DOI={10.1017/S0956796800000885},
  number={4},
  journal={Journal of Functional Programming},
  publisher={Cambridge University Press},
  author={Adams, Stephen},
  year={1993},
  pages={553–561}
}
@article{debruijn,
  title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
  journal = {Indagationes Mathematicae (Proceedings)},
  volume = {75},
  number = {5},
  pages = {381-392},
  year = {1972},
  issn = {1385-7258},
  doi = {https://doi.org/10.1016/1385-7258(72)90034-0},
  author = {N.G {de Bruijn}},
}
@phdthesis{santos,
   abstract = {In this thesis we present and analyse a set of automatic source-to-source\nprogram transformations that are suitable for incorporation in optimising\ncompilers for lazy functional languages. These transformations improve\nthe quality of code in many different respects, such as execution\ntime and memory usage. The transformations presented are divided\nin two sets: global transformations, which are performed once (or\nsometimes twice) during the compilation process; and a set of local\ntransformations, which are performed before and after each of the\nglobal transformations, so that they can simplify the code before\napplying the global transformations and also take advantage of them\nafterwards. Many of the local transformations are simple, well known,\nand do not have major effects on their own. They become important\nas they interact with each other and with global transformations,\nsometimes in non-obvious ways. We present how and why they improve\nthe code, and perform extensive experiments with real application\nprograms. We describe four global transformations, two of which have\nnot been used in any lazy functional compiler we know of: the static\nargument transformation and let foating transformations. The other\ntwo are well known transformations for lazy functional languages,\nbut for which no major studies of their e ects have been performed:\nfull laziness and lambda lifting. We also study and measure the e\nects of di erent inlining strategies.\n\nWe also present a Cost Semantics as a way of reasoning about the e\nects of program transformations in lazy functional languages.},
   author = {André Luís De Medeiros Santos},
   school = {University of Glasgow},
   title = {Compilation by Transformation in Non-Strict Functional Languages},
   year = {1995},
}
@article{hinze:generalized,
  author    = {Ralf Hinze},
  title     = {Generalizing Generalized Tries},
  journal   = {Journal of Functional Programming},
  journal   = {J. Funct. Program.},
  volume    = {10},
  number    = {4},
  pages     = {327--351},
  year      = {2000},
  url       = {http://journals.cambridge.org/action/displayAbstract?aid=59745},
  timestamp = {Fri, 10 Jun 2011 14:42:13 +0200},
  biburl    = {https://dblp.org/rec/journals/jfp/Hinze00a.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{handbook:2001,
  author = {R Sekar and IV Ramakrishnan and A Voronkov},
  title = {Handbook of Automated Reasoning},
  volume = {2},
  year = {2001},
  publisher = {Elsevier}
}

@article{voronkov:vampire,
 author = {A Voronkov},
 title = {The anatomy of Vampire: Implementing bottom-up procedures with code trees},
 journal = {Journal of Automated Reasoning},
 volume = {15}, issue = {2},
 pages = {237-265},
 year = {1995}
}

@inproceedings{substitution-trees,
  author = {Graf, P and Meyer, C},
  title = {Advanced indexing operations on substitution trees},
  booktitle = {Proc International Conference on Automated Deduction (CADE'96), LNCS 1104},
  editor = {McRobbie, MA and Slaney JK},
  year = {1996},
  page = {553–567},
  publisher = {Springer}
}

@inproceedings{e-matching-code-trees,
  author = {Leonardo de Moura and Nikolaj Bjørner},
  title = {Efficient E-Matching for SMT solvers},
  booktitle = {Proc International Conference on Automated Deduction (CADE)},
  pages = {183-198},
  publisher = {Springer},
  year = {2007}
}

@inproceedings{spass,
  author = {Weidenbach, Christoph and Dimova, Dilyana and Fietzke, Arnaud and Kumar, Rohit and Suda, Martin and Wischnewski, Patrick},
  year = {2009},
  title = {SPASS Version 3.5},
  booktitle = {Proc International Conference on Automated Deduction (CADE)},
  publisher = {Springer},
  pages = {140–145}
}

@inproceedings{associated-types,
author = {Chakravarty, Manuel M. T. and Keller, Gabriele and Jones, Simon Peyton},
title = {Associated Type Synonyms},
year = {2005},
isbn = {1595930647},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1086365.1086397},
doi = {10.1145/1086365.1086397},
abstract = {Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developing earlier work on associated data types, we propose to add functionally dependent types as type synonyms to type-class bodies. These associated type synonyms constitute an interesting new alternative to explicit functional dependencies.},
booktitle = {Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming},
pages = {241–253},
numpages = {13},
keywords = {associated types, type classes, type inference, generic programming, type functions},
location = {Tallinn, Estonia},
series = {ICFP '05}
}

@InProceedings{rewrite-rules,
author = {Peyton Jones, Simon and Tolmach, Andrew and Hoare, Tony},
title = {Playing by the rules: rewriting as a practical optimisation technique in GHC},
organization = {ACM SIGPLAN},
booktitle = {2001 Haskell Workshop},
year = {2001},
month = {September},
publisher = {ACM},
abstract = {We describe a facility for improving optimization of Haskell programs using rewrite rules. Library authors can use rules to express domain-specific optimizations that the compiler cannot discover for itself. The compiler can also generate rules internally to propagate information obtained from automated analyses. The rewrite mechanism is fully implemented in the released Glasgow Haskell Compiler.

Our system is very simple, but can be effective in optimizing real programs. We describe two practical applications involving short-cut deforestation, for lists and for rose trees, and document substantial performance improvements on a range of programs.},
url = {https://www.microsoft.com/en-us/research/publication/playing-by-the-rules-rewriting-as-a-practical-optimisation-technique-in-ghc/},
edition = {2001 Haskell Workshop},
}

@misc{conal:blog1,
  title = {Elegant memoization with functional memo tries},
  author = {Conal Elliott},
  year = {2008},
  howpublished = {\url{http://conal.net/blog/posts/elegant-memoization-with-functional-memo-tries}},
}

@misc{conal:blog2,
  title = {Composing memo tries},
  author = {Conal Elliott},
  year = {2008},
  howpublished = {\url{http://conal.net/blog/posts/composing-memo-tries}},
}

@INPROCEEDINGS{hinze:memo,
    author = {Ralf Hinze},
    title = {Memo Functions, Polytypically!},
    booktitle = {Proceedings of the 2nd Workshop on Generic Programming, Lima‚ Portugal},
    year = {2000},
    pages = {17--32}
}

@InProceedings{alpha-hashing,
author = {Maziarz, Krzysztof and Ellis, Tom and Lawrence, Alan and Fitzgibbon, Andrew and Peyton Jones, Simon},
title = {Hashing Modulo Alpha-Equivalence},
organization = {ACM},
booktitle = {ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21)},
year = {2021},
month = {June},
abstract = {In many applications one wants to identify identical subtrees of a program syntax tree.  This identification should ideally be robust to alpha-renaming of the program, but no existing technique has been shown to achieve this with good efficiency (better than O(n^2) in expression size). We present a new, asymptotically efficient way to hash modulo alpha-equivalence. A key insight of our method is to use a weak (commutative) hash combiner at exactly one point in the construction, which admits an algorithm with O(n*(log n)^2) time complexity. We prove that the use of the commutative combiner nevertheless yields a strong hash with low collision probability.},
publisher = {ACM},
url = {https://www.microsoft.com/en-us/research/publication/hashing-modulo-alpha-equivalence-2/},
}

@article{discr-sort,
author = {Henglein, Fritz},
title = {Generic Discrimination: Sorting and Paritioning Unshared Data in Linear Time},
year = {2008},
issue_date = {September 2008},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {43},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/1411203.1411220},
doi = {10.1145/1411203.1411220},
journal = {SIGPLAN Not.},
month = sep,
pages = {91–102},
numpages = {12},
keywords = {sorting, order, total preorder, partitioning, generic, equivalence, discriminator, functional, multiset discrimination, discrimination}
}