bibliography.bib

@article{jones1992,
author = {Jones, Peyton and L, Simon and Peyton Jones, Simon},
title = {Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-machine},
year = {1992},
month = {July},
abstract = {The Spineless Tagless G-machine is an abstract machine designed to support non- strict higher-order functional languages. This presentation of the machine falls into three parts. Firstly, we give a general discussion of the design issues involved in implementing non-strict functional languages.
Next, we present the STG language, an austere but recognisably-functional language, which as well as a denotational meaning has a well-defined operational semantics. The STG language is the \abstract machine code" for the Spineless Tagless G-machine.
Lastly, we discuss the mapping of the STG language onto stock hardware. The success of an abstract machine model depends largely on how efficient this mapping can be made, though this topic is often relegated to a short section. Instead, we give a detailed discussion of the design issues and the choices we have made. Our principal target is the C language, treating the C compiler as a portable assembler.},
publisher = {Cambridge University Press},
url = {https://www.microsoft.com/en-us/research/publication/implementing-lazy-functional-languages-on-stock-hardware-the-spineless-tagless-g-machine/},
pages = {127-202},
journal = {Journal of Functional Programming},
volume = {2},
edition = {Journal of Functional Programming},
}

@inproceedings{boquist1996,
author = {Boquist, Urban and Johnsson, Thomas},
title = {The GRIN Project: A Highly Optimising Back End for Lazy Functional Languages},
year = {1996},
isbn = {3540632379},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
booktitle = {Selected Papers from the 8th International Workshop on Implementation of Functional Languages},
pages = {58–84},
numpages = {27},
series = {IFL '96}
}

@book{aho2006,
author = {Aho, Alfred V. and Lam, Monica S. and Sethi, Ravi and Ullman, Jeffrey D.},
title = {Compilers: Principles, Techniques, and Tools (2nd Edition)},
year = {2006},
isbn = {0321486811},
publisher = {Addison-Wesley Longman Publishing Co., Inc.},
address = {USA}
}



@phdthesis{boquist1999,
  author       = {Urban Boquist},
  title        = {Code Optimisation Techniques for Lazy Functional Languages},
  school       = {Chalmers University of Technology, Gothenburg, Sweden},
  year         = {1999},
  url          = {http://publications.lib.chalmers.se/publication/890-code-optimisation-techniques-for-lazy-functional-languages},
}




@inproceedings{ullrich2021,
author = {Ullrich, Sebastian and de Moura, Leonardo},
title = {Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming},
year = {2021},
isbn = {9781450375627},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3412932.3412935},
doi = {10.1145/3412932.3412935},
booktitle = {Proceedings of the 31st Symposium on Implementation and Application of Functional Languages},
articleno = {3},
numpages = {12},
keywords = {lean, reference counting, purely functional programming},
location = {Singapore, Singapore},
series = {IFL '19}
}

@techreport{reinking2020,
author = {Reinking*, Alex and Xie*, Ningning and de Moura, Leonardo and Leijen, Daan},
title = {Perceus: Garbage Free Reference Counting with Reuse (Extended version)},
institution = {Microsoft},
year = {2020},
month = {November},
url = {https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/},
number = {MSR-TR-2020-42},
note = {(*) The first two authors contributed equally to this work. v4, 2021-06-07. Extended version of the PLDI'21 paper.},
}

@inproceedings{reinking2021,
author = {Reinking, Alex and Xie, Ningning and de Moura, Leonardo and Leijen, Daan},
title = {Perceus: Garbage Free Reference Counting with Reuse},
year = {2021},
isbn = {9781450383912},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3453483.3454032},
doi = {10.1145/3453483.3454032},
abstract = {We introduce Perceus, an algorithm for precise reference counting with reuse and specialization. Starting from a functional core language with explicit control-flow, Perceus emits precise reference counting instructions such that (cycle-free) programs are _garbage free_, where only live references are retained. This enables further optimizations, like reuse analysis that allows for guaranteed in-place updates at runtime. This in turn enables a novel programming paradigm that we call _functional but in-place_ (FBIP). Much like tail-call optimization enables writing loops with regular function calls, reuse analysis enables writing in-place mutating algorithms in a purely functional way. We give a novel formalization of reference counting in a linear resource calculus, and prove that Perceus is sound and garbage free. We show evidence that Perceus, as implemented in Koka, has good performance and is competitive with other state-of-the-art memory collectors.},
booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
pages = {96–111},
numpages = {16},
keywords = {Handlers, Algebraic Effects, Reference Counting},
location = {Virtual, Canada},
series = {PLDI 2021}
}

@article{lorenzen2022,
author = {Lorenzen, Anton and Leijen, Daan},
title = {Reference Counting with Frame Limited Reuse},
year = {2022},
issue_date = {August 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {ICFP},
url = {https://doi.org/10.1145/3547634},
doi = {10.1145/3547634},
journal = {Proc. ACM Program. Lang.},
month = {8},
articleno = {103},
numpages = {24},
keywords = {Frame Limited, Reference Counting, Reuse, Koka}
}

@techreport{lorenzen2023,
author = {Lorenzen, Anton and Leijen, Daan and Swierstra, Wouter},
title = {FP$^2$: Fully in-Place Functional Programming},
institution = {Microsoft},
year = {2023},
month = {5},
url = {https://www.microsoft.com/en-us/research/publication/fp2-fully-in-place-functional-programming/},
number = {MSR-TR-2023-19},
}

@inproceedings{hage2008,
author = {Hage, Jurriaan and Holdermans, Stefan},
title = {Heap Recycling for Lazy Languages},
year = {2008},
isbn = {9781595939777},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1328408.1328436},
doi = {10.1145/1328408.1328436},
abstract = {Pure functional programming languages preclude destructive updates of heap-allocated data. In such languages, all newly computed algebraic values claim freshly allocated heap space, which typically causes idiomatic programs to be notoriously inefficient when compared to their imperative and impure counterparts. We partly overcome this shortcoming by considering a syntactically light language construct for enabling user-controlled in-place updates of algebraic values. The resulting calculus, that is based on a combination of type-based uniqueness and constructor analysis, is guaranteed to maintain referential transparency and is fully compatible with existing run-time systems for nonstrict, pure functional languages.},
booktitle = {Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
pages = {189–197},
numpages = {9},
keywords = {lazy functional programming, compile-time garbage collection, type-based program analysis},
location = {San Francisco, California, USA},
series = {PEPM '08}
}

@inproceedings{ende2010,
  title={Extending the UHC LLVM backend : Adding support for accurate garbage collection},
  author={P v.d. Ende},
  year={2010}
}

@inproceedings{dijkstra2009,
author = {Dijkstra, Atze and Fokker, Jeroen and Swierstra, S. Doaitse},
title = {The Architecture of the Utrecht Haskell Compiler},
year = {2009},
isbn = {9781605585086},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1596638.1596650},
doi = {10.1145/1596638.1596650},
abstract = {In this paper we describe the architecture of the Utrecht Haskell Compiler (UHC).UHC is a new Haskell compiler, that supports most (but not all) Haskell 98 features, plus some experimental extensions. It targets multiple backends, including a bytecode interpreter backend and a whole-program analysis backend, both via C. The implementation is rigorously organized as stepwise transformations through some explicit intermediate languages. The tree walks of all transformations are expressed as an algebra, with the aid of an Attribute Grammar based preprocessor. The compiler is just one materialization of a framework that supports experimentation with language variants, thanks to an aspect-oriented internal organization.},
booktitle = {Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell},
pages = {93–104},
numpages = {12},
keywords = {aspect orientation, attribute grammar, compiler architecture, haskell},
location = {Edinburgh, Scotland},
series = {Haskell '09}
}

@inproceedings{boeijink2010,
  title={Introducing the PilGRIM: A Processor for Executing Lazy Functional Languages},
  author={Arjan Boeijink and Philip K. F. H{\"o}lzenspies and Jan Kuper},
  booktitle={International Symposium on Implementation and Application of Functional Languages},
  year={2010}
}

@article{johnsson2004,
author = {Johnsson, Thomas},
title = {Efficient Compilation of Lazy Evaluation},
year = {2004},
issue_date = {April 2004},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {39},
number = {4},
issn = {0362-1340},
url = {https://doi.org/10.1145/989393.989409},
doi = {10.1145/989393.989409},
abstract = {This paper describes the principles underlying an efficient implementation of a lazy functional language, compiling to code for ordinary computers. It is based on combinator-like graph reduction: the user defined functions are used as rewrite rules in the graph. Each function is compiled into an instruction sequence for an abstract graph reduction machine, called the G-machine, the code reduces a function application graph to its value. The G-machine instructions are then translated into target code. Speed improvements by almost two orders of magnitude over previous lazy evaluators have been measured; we provide some performance figures.},
journal = {SIGPLAN Not.},
month = {apr},
pages = {125–138},
numpages = {14}
}

@inproceedings{okabe2014,
author = {Okabe, Kiwamu and Muranushi, Takayuki},
title = {Systems Demonstration: Writing NetBSD Sound Drivers in Haskell},
year = {2014},
isbn = {9781450330411},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2633357.2633370},
doi = {10.1145/2633357.2633370},
abstract = {Most strongly typed, functional programming languages are not equipped with a reentrant garbage collector. Therefore such languages are not used for operating systems programming, where the virtues of types are most desired. We propose the use of Context-Local Heaps (CLHs) to achieve reentrancy, which also increasing the speed of garbage collection. We have implemented CLHs in Ajhc, a Haskell compiler derived from jhc, rewritten some NetBSD sound drivers using Ajhc, and benchmarked them. The reentrant, faster garbage collection that CLHs provide opens the path to type-assisted operating systems programming.},
booktitle = {Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell},
pages = {77–78},
numpages = {2},
keywords = {performance, languages},
location = {Gothenburg, Sweden},
series = {Haskell '14}
}

@article{xi2018,
  author       = {Hongwei Xi and
                  Dengping Zhu},
  title        = {To Memory Safety through Proofs},
  journal      = {CoRR},
  volume       = {abs/1810.12190},
  year         = {2018},
  url          = {http://arxiv.org/abs/1810.12190},
  eprinttype    = {arXiv},
  eprint       = {1810.12190},
  timestamp    = {Thu, 01 Nov 2018 18:03:07 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1810-12190.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{racordon2022,
  title={Implementation Strategies for Mutable Value Semantics},
  author={Dimitri Racordon and Denys Shabalin and Daniel Zheng and Dave Abrahams and Brennan Saeta},
  journal={J. Object Technol.},
  year={2022},
  volume={21},
  pages={2:1-11},
  url={https://api.semanticscholar.org/CorpusID:248335097}
}

@misc{racordon2021,
  title={Native Implementation of Mutable Value Semantics}, 
  author={Dimitri Racordon and Denys Shabalin and Daniel Zheng and Dave Abrahams and Brennan Saeta},
  year={2021},
  eprint={2106.12678},
  archivePrefix={arXiv},
  primaryClass={cs.PL}
}

@inproceedings{boquist1995,
author = {Boquist, Urban},
title = {Interprocedural Register Allocation for Lazy Functional Languages},
year = {1995},
isbn = {0897917197},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/224164.224215},
doi = {10.1145/224164.224215},
booktitle = {Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture},
pages = {270–281},
numpages = {12},
location = {La Jolla, California, USA},
series = {FPCA '95}
}

@article{collins1960,
author = {Collins, George E.},
title = {A Method for Overlapping and Erasure of Lists},
year = {1960},
issue_date = {Dec. 1960},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {12},
issn = {0001-0782},
url = {https://doi.org/10.1145/367487.367501},
doi = {10.1145/367487.367501},
abstract = {An important property of the Newell Shaw-Simon scheme for computer storage of lists is that data having multiple occurrences need not be stored at more than one place in the computer. That is, lists may be “overlapped.” Unfortunately, overlapping poses a problem for subsequent erasure. Given a list that is no longer needed, it is desired to erase just those parts that do not overlap other lists. In LISP, McCarthy employs an elegant but inefficient solution to the problem. The present paper describes a general method which enables efficient erasure. The method employs interspersed reference counts to describe the extent of the overlapping.},
journal = {Commun. ACM},
month = {dec},
pages = {655–657},
numpages = {3}
}

@article{appel1997, title={Garbage Collection: Algorithms for Automatic Dynamic Memory Management by Richard Jones and Rafael Lins, John Wiley & Sons, 1996.}, volume={7}, DOI={10.1017/S0956796897212682}, number={2}, journal={Journal of Functional Programming}, publisher={Cambridge University Press}, author={APPEL, ANDREW W.}, year={1997}, pages={227–229}}

@book{jones1996,
author = {Jones, Richard and Lins, Rafael},
title = {Garbage Collection: Algorithms for Automatic Dynamic Memory Management},
year = {1996},
isbn = {0471941484},
publisher = {John Wiley \& Sons, Inc.},
address = {USA}
}

@article{peytonjones1992, title={Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine}, volume={2}, DOI={10.1017/S0956796800000319}, number={2}, journal={Journal of Functional Programming}, publisher={Cambridge University Press}, author={Jones, Simon L. Peyton}, year={1992}, pages={127–202}}

@inproceedings{wilson1992,
  title={Uniprocessor Garbage Collection Techniques},
  author={Paul R. Wilson},
  booktitle={IWMM},
  year={1992},
  url={https://api.semanticscholar.org/CorpusID:206841815}
}

@unpublished{pinto2023,
author = {Pinto, Elton and Leijen, Daan},
title = {Exploring Perceus for OCaml},
year = {2023},
month = {September},
abstract = {The Perceus algorithm is a precise and garbage-free reference counting scheme which shows good performance in practice. However, the algorithm has only been compared against garbage-collection across different systems and languages. There is no direct comparison between Perceus and a garbage collector within the same system.

In this work, we take an initial step towards this goal. We have implemented a prototype of Perceus for OCaml 4.14.0 (which subsumes the standard garbage collector). Now we can directly compare the performance of programs compiled with the exact same compiler, where we only switch the backend: either using the standard generational collector, or using Perceus compilation with a reference counted runtime system. The initial performance results look quite promising, motivating futher exploration.},
url = {https://www.microsoft.com/en-us/research/publication/exploring-perceus-for-ocaml/},
note = {Presented at the "Higher order, Typed, Strict: ML Family Workshop 2023" co-located with ICFP'23.},
}

@article{lorenzen2021,
  title={Optimizing Reference Counting with Borrowing},
  author={Lorenzen, Anton Felix},
  year={2021},
  url={https://antonlorenzen.de/master_thesis_perceus_borrowing.pdf}
}


@InProceedings{johnsson1991,
author="Johnsson, Thomas",
editor="Jones, Simon L. Peyton
and Hutton, Graham
and Holst, Carsten Kehler",
title="Analysing Heap Contents in a Graph Reduction Intermediate Language",
booktitle="Functional Programming, Glasgow 1990",
year="1991",
publisher="Springer London",
address="London",
pages="146--171",
abstract="We present an algorithm to analyse graph reduction intermediate code, which gives a safe approximation to what kind of nodes (i.e. which constructors and/or unevaluated function applications) pointers might point to at different points in the program. The analysed language, called GRIN (Graph Reduction Intermediate Notation) is a procedural language with operations essentially the same as in the G-machine but in the form of three address instructions. The analysis uses a framework developed by Jones and Muchnick for dealing with the interprocedural flow of information.",
isbn="978-1-4471-3810-5"
}

@InProceedings{davis1991,
author="Davis, Kei
and Wadler, Philip",
editor="Jones, Simon L. Peyton
and Hutton, Graham
and Holst, Carsten Kehler",
title="Strictness Analysis in 4D",
booktitle="Functional Programming, Glasgow 1990",
year="1991",
publisher="Springer London",
address="London",
pages="23--43",
abstract="Strictness analysis techniques can be classified along four different dimensions: first-order vs. higher-order, flat vs. non-flat, low fidelity vs. high fidelity, and forward vs. backward. Plotting a table of the positions of known techniques within this space reveals that certain regions are densely occupied while others are empty. In particular, techniques for high-fidelity forward and low-fidelity backward analysis are well known, while those for low-fidelity forward and high-fidelity backward analysis are lacking. This paper fills in the gaps: the low-fidelity forward methods provide faster analyses than the high-fidelity forward methods, at the cost of accuracy, while the high-fidelity backward methods provide more information than the low-fidelity backward methods, at the cost of time.",
isbn="978-1-4471-3810-5"
}

@inproceedings{jonsson2008,
   author = {Jonsson, Peter A. and Nordlander, Johan},
   institution = {Luleå University of Technology, Embedded Internet Systems Lab},
   institution = {Luleå University of Technology, Computer Science},
   note = {Godk{\"a}nd; 2008; 20081022 (pj)},
   title = {On building a supercompiler for GHC},
   abstract = {Supercompilation is a program transformation that removes intermediate structures and performs program  specialization. We discuss problems and necessary steps for building a supercompiler for GHC. },
   year = {2008}
}

@article{bolingbroke2010,
author = {Bolingbroke, Maximilian and Peyton Jones, Simon},
title = {Supercompilation by Evaluation},
year = {2010},
issue_date = {November 2010},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {45},
number = {11},
issn = {0362-1340},
url = {https://doi.org/10.1145/2088456.1863540},
doi = {10.1145/2088456.1863540},
abstract = {This paper shows how call-by-need supercompilation can be recast to be based explicitly on an evaluator, contrasting with standard presentations which are specified as algorithms that mix evaluation rules with reductions that are unique to supercompilation. Building on standard operational-semantics technology for call-by-need languages, we show how to extend the supercompilation algorithm to deal with recursive let expressions.},
journal = {SIGPLAN Not.},
month = {sep},
pages = {135–146},
numpages = {12},
keywords = {haskell, specialisation, deforestation, optimisation, supercompilation}
}

@article{podlovics2021, 
title={A Modern Look at GRIN, an Optimizing Functional Language Back End}, 
volume={25}, 
url={https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/4101}, 
DOI={10.14232/actacyb.282969}, 
abstractNote={<p>GRIN is short for Graph Reduction Intermediate Notation, a modern back end for lazy functional languages. Most of the currently available compilers for such languages share a common flaw: they can only optimize programs on a per-module basis. The GRIN framework allows for interprocedural whole program analysis, enabling optimizing code transformations across functions and modules as well.</p> <p>Some implementations of GRIN already exist, but most of them were developed only for experimentation purposes. Thus, they either compromise on low-level efficiency or contain ad hoc modifications compared to the original specification.</p> <p>Our goal is to provide a full-fledged implementation of GRIN by combining the currently available best technologies like LLVM, and evaluate the framework’s effectiveness by measuring how the optimizer improves the performance of certain programs. We also present some improvements to the already existing components of the framework. Some of these improvements include a typed representation for the intermediate language and an interprocedural program optimization, the dead data elimination.</p>}, 
number={4}, 
journal={Acta Cybernetica}, 
author={Podlovics, Peter and Hruska, Csaba and Pénzes, Andor}, 
year={2021}, 
month={Feb.}, 
pages={847-876} 
}

@inproceedings{petersen2013,
author = {Petersen, Leaf and Anderson, Todd A. and Liu, Hai and Glew, Neal},
title = {Measuring the Haskell Gap},
year = {2013},
isbn = {9781450329880},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2620678.2620685},
doi = {10.1145/2620678.2620685},
abstract = {Papers on functional language implementations frequently set the goal of achieving performance "comparable to C", and sometimes report results comparing benchmark results to concrete C implementations of the same problem. A key pair of questions for such comparisons is: what C program to compare to, and what C compiler to compare with? In a 2012 paper, Satish et al [9] compare naive serial C implementations of a range of throughput-oriented benchmarks to best-optimized implementations parallelized on a six-core machine and demonstrate an average 23X (up to 53X) speedup. Even accounting for thread parallel speedup, these results demonstrate a substantial performance gap between naive and tuned C code. In this current paper, we choose a subset of the benchmarks studied by Satish et al to port to Haskell. We measure performance of these Haskell benchmarks compiled with the standard Glasgow Haskell Compiler and with our experimental Intel Labs Haskell Research Compiler and report results as compared to our best reconstructions of the algorithms used by Satish et al. Results are reported as measured both on an Intel Xeon E5-4650 32-core machine, and on an Intel Xeon Phi co-processor. We hope that this study provides valuable data on the concrete performance of Haskell relative to C.},
booktitle = {Proceedings of the 25th Symposium on Implementation and Application of Functional Languages},
pages = {61–72},
numpages = {12},
location = {Nijmegen, Netherlands},
series = {IFL '13}
}

@inproceedings{liu2013,
author = {Liu, Hai and Glew, Neal and Petersen, Leaf and Anderson, Todd A.},
title = {The Intel Labs Haskell Research Compiler},
year = {2013},
isbn = {9781450323833},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2503778.2503779},
doi = {10.1145/2503778.2503779},
abstract = {The Glasgow Haskell Compiler (GHC) is a well supported optimizing compiler for the Haskell programming language, along with its own extensions to the language and libraries. Haskell's lazy semantics imposes a runtime model which is in general difficult to implement efficiently. GHC achieves good performance across a wide variety of programs via aggressive optimization taking advantage of the lack of side effects, and by targeting a carefully tuned virtual machine. The Intel Labs Haskell Research Compiler uses GHC as a frontend, but provides a new whole-program optimizing backend by compiling the GHC intermediate representation to a relatively generic functional language compilation platform. We found that GHC's external Core language was relatively easy to use, but reusing GHC's libraries and achieving full compatibility were harder. For certain classes of programs, our platform provides substantial performance benefits over GHC alone, performing 2x faster than GHC with the LLVM backend on selected modern performance-oriented benchmarks; for other classes of programs, the benefits of GHC's tuned virtual machine continue to outweigh the benefits of more aggressive whole program optimization. Overall we achieve parity with GHC with the LLVM backend. In this paper, we describe our Haskell compiler stack, its implementation and optimization approach, and present benchmark results comparing it to GHC.},
booktitle = {Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell},
pages = {105–116},
numpages = {12},
keywords = {compiler optimization, haskell, functional language compiler},
location = {Boston, Massachusetts, USA},
series = {Haskell '13}
}

@InProceedings{bergstrom2010,
author="Bergstrom, Lars
and Reppy, John",
editor="Moraz{\'a}n, Marco T.
and Scholz, Sven-Bodo",
title="Arity Raising in Manticore",
booktitle="Implementation and Application of Functional Languages",
year="2010",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="90--106",
abstract="Compilers for polymorphic languages are required to treat values in programs in an abstract and generic way at the source level. The challenges of optimizing the boxing of raw values, flattening of argument tuples, and raising the arity of functions that handle complex structures to reduce memory usage are old ones, but take on newfound import with processors that have twice as many registers. We present a novel strategy that uses both control-flow and type information to provide an arity raising implementation addressing these problems. This strategy is conservative --- no matter the execution path, the transformed program will not perform extra operations.",
isbn="978-3-642-16478-1"
}

@article{kaser1997, 
title={EQUALS – a fast parallel implementation of a lazy language}, 
volume={7}, 
DOI={10.1017/S0956796897002669}, 
number={2}, 
journal={Journal of Functional Programming}, 
publisher={Cambridge University Press}, 
author={Kaser, Owen and Ramakrishnan, C. R. and Ramakrishnan, I. V. and Sekar, R. C.}, 
year={1997}, 
pages={183–217}
}

@inproceedings{johnsson1984,
author = {Johnsson, Thomas},
title = {Efficient Compilation of Lazy Evaluation},
year = {1984},
isbn = {0897911393},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/502874.502880},
doi = {10.1145/502874.502880},
abstract = {This paper describes the principles underlying an efficient implementation of a lazy functional language, compiling to code for ordinary computers. It is based on combinator-like graph reduction: the user defined functions are used as rewrite rules in the graph. Each function is compiled into an instruction sequence for an abstract graph reduction machine, called the G-machine, the code reduces a function application graph to its value. The G-machine instructions are then translated into target code. Speed improvements by almost two orders of magnitude over previous lazy evaluators have been measured; we provide some performance figures.},
booktitle = {Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction},
pages = {58–69},
numpages = {12},
location = {Montreal, Canada},
series = {SIGPLAN '84}
}

@inproceedings{wadler1984,
author = {Wadler, Philip},
title = {Listlessness is Better than Laziness: Lazy Evaluation and Garbage Collection at Compile-Time},
year = {1984},
isbn = {0897911423},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/800055.802020},
doi = {10.1145/800055.802020},
booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
pages = {45–52},
numpages = {8},
location = {Austin, Texas, USA},
series = {LFP '84}
}

@inproceedings{wadler1988,
author = {Wadler, Philip},
title = {Deforestation: Transforming Programs to Eliminate Trees},
year = {1988},
publisher = {North-Holland Publishing Co.},
address = {NLD},
booktitle = {Proceedings of the Second European Symposium on Programming},
pages = {231–248},
numpages = {18},
location = {Nancy, France}
}

@mastersthesis{teeuwissen2023,
author = {Teeuwissen, J.},
year={2023},
title={Reference Counting with Reuse in Roc},
url = {https://studenttheses.uu.nl/handle/20.500.12932/44634},
school={Utrecht University}
}

@article{ho2023,
author = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan},
title = {Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification},
year = {2023},
issue_date = {August 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {ICFP},
url = {https://doi.org/10.1145/3607844},
doi = {10.1145/3607844},
abstract = {For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-scale proof developments. We present the design, implementation and evaluation of a set of language-based techniques that allow the programmer to modularly write and verify code at a high level of abstraction, while retaining control over the compilation process and producing high-quality, zero-overhead, low-level code suitable for integration into mainstream software. We implement our techniques within the F proof assistant, and specifically its shallowly-embedded Low toolchain that compiles to C. Through our evaluation, we establish that our techniques were critical in scaling the popular HACL library past 100,000 lines of verified source code, and brought about significant gains in proof engineer productivity. The exposition of our methodology converges on one final, novel case study: the streaming API, a finicky API that has historically caused many bugs in high-profile software. Using our approach, we manage to capture the streaming semantics in a generic way, and apply it “for free” to over a dozen use-cases. Six of those have made it into the reference implementation of the Python programming language, replacing the previous CVE-ridden code.},
journal = {Proc. ACM Program. Lang.},
month = {aug},
articleno = {202},
numpages = {32},
keywords = {Cryptographic Primitives, Proof Engineering}
}

@inproceedings{johnson2017,
author = {Johnson, Teresa and Amini, Mehdi and Li, Xinliang David},
title = {ThinLTO: Scalable and Incremental LTO},
year = {2017},
isbn = {9781509049318},
publisher = {IEEE Press},
abstract = {Cross-Module Optimization (CMO) is an effective means for improving runtime performance, by extending the scope of optimizations across source module boundaries. Two CMO approaches are Link-Time Optimization (LTO) and Lightweight Inter-Procedural Optimization (LIPO). However, each of these solutions has limitations that prevent it from being enabled by default. ThinLTO is a new approach that attempts to address these limitations, with a goal of being enabled more broadly. ThinLTO aims to be as scalable as a regular non-LTO build, enabling CMO on large applications and machines without large memory configurations, while also integrating well with distributed and incremental build systems. This is achieved through fast purely summary-based Whole-Program Analysis (WPA), the only serial step, without reading or writing the program’s Intermediate Representation (IR). Instead, CMO is applied during fully parallel optimization backends. This paper describes the motivation behind ThinLTO, its overall design, and current implementation in LLVM. Results from SPEC cpu2006 benchmarks and several large real-world applications illustrate that ThinLTO can scale as well as a non-LTO build while enabling most of the CMO performed with a full LTO build.},
booktitle = {Proceedings of the 2017 International Symposium on Code Generation and Optimization},
pages = {111–121},
numpages = {11},
keywords = {Optimization, Cross-module, Inter-procedural, Link-Time Optimization},
location = {Austin, USA},
series = {CGO '17}
}

@article{brandon2023,
author = {Brandon, William and Driscoll, Benjamin and Dai, Frank and Berkow, Wilson and Milano, Mae},
title = {Better Defunctionalization through Lambda Set Specialization},
year = {2023},
issue_date = {June 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {PLDI},
url = {https://doi.org/10.1145/3591260},
doi = {10.1145/3591260},
abstract = {Higher-order functions pose a challenge for both static program analyses and optimizing compilers. To simplify the analysis and compilation of languages with higher-order functions, a rich body of prior work has proposed a variety of defunctionalization techniques, which can eliminate higher-order functions from a program by transforming the program to a semantically-equivalent first-order representation. Several modern languages take this a step further, specializing higher-order functions with respect to the functions on which they operate, and in turn allowing compilers to generate more efficient code. However, existing specializing defunctionalization techniques restrict how function values may be used, forcing implementations to fall back on costly dynamic alternatives. We propose lambda set specialization (LSS), the first specializing defunctionalization technique which imposes no restrictions on how function values may be used. We formulate LSS in terms of a polymorphic type system which tracks the flow of function values through the program, and use this type system to recast specialization of higher-order functions with respect to their arguments as a form of type monomorphization. We show that our type system admits a simple and tractable type inference algorithm, and give a formalization and fully-mechanized proof in the Isabelle/HOL proof assistant showing soundness and completeness of the type inference algorithm with respect to the type system. To show the benefits of LSS, we evaluate its impact on the run time performance of code generated by the MLton compiler for Standard ML, the OCaml compiler, and the new Morphic functional programming language. We find that pre-processing with LSS achieves run time speedups of up to 6.85x under MLton, 3.45x for OCaml, and 78.93x for Morphic.},
journal = {Proc. ACM Program. Lang.},
month = {jun},
articleno = {146},
numpages = {24},
keywords = {type systems, monomorphization, defunctionalization}
}

@article{huang2023,
author = {Huang, Yulong and Yallop, Jeremy},
title = {Defunctionalization with Dependent Types},
year = {2023},
issue_date = {June 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {PLDI},
url = {https://doi.org/10.1145/3591241},
doi = {10.1145/3591241},
abstract = {The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied. We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages},
journal = {Proc. ACM Program. Lang.},
month = {jun},
articleno = {127},
numpages = {23},
keywords = {type preservation, compilation, type systems, dependent types}
}
@article{kovacs2020,
author = {Kov\'{a}cs, Andr\'{a}s},
title = {Elaboration with First-Class Implicit Function Types},
year = {2020},
issue_date = {August 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {ICFP},
url = {https://doi.org/10.1145/3408983},
doi = {10.1145/3408983},
abstract = {Implicit functions are dependently typed functions, such that arguments are provided (by default) by inference machinery instead of programmers of the surface language. Implicit functions in Agda are an archetypal example. In the Haskell language as implemented by the Glasgow Haskell Compiler (GHC), polymorphic types are another example. Implicit function types are first-class if they are treated as any other type in the surface language. This holds in Agda and partially holds in GHC. Inference and elaboration in the presence of first-class implicit functions poses a challenge; in the context of Haskell and ML-like languages, this has been dubbed “impredicative instantiation” or “impredicative inference”. We propose a new solution for elaborating first-class implicit functions, which is applicable to full dependent type theories and compares favorably to prior solutions in terms of power, generality and simplicity. We build atop Norell’s bidirectional elaboration algorithm for Agda, and we note that the key issue is incomplete information about insertions of implicit abstractions and applications. We make it possible to track and refine information related to such insertions, by adding a function type to a core Martin-L'of type theory, which supports strict (definitional) currying. This allows us to represent undetermined domain arities of implicit function types, and we can decide at any point during elaboration whether implicit abstractions should be inserted.},
journal = {Proc. ACM Program. Lang.},
month = {aug},
articleno = {101},
numpages = {29},
keywords = {impredicative polymorphism, type theory, type inference, elaboration}
}

@inproceedings{sparud1993,
author = {Sparud, Jan},
title = {Fixing Some Space Leaks without a Garbage Collector},
year = {1993},
isbn = {089791595X},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/165180.165196},
doi = {10.1145/165180.165196},
booktitle = {Proceedings of the Conference on Functional Programming Languages and Computer Architecture},
pages = {117–122},
numpages = {6},
location = {Copenhagen, Denmark},
series = {FPCA '93}
}


@article{hamilton1998,
title = {Usage Counting Analysis for Lazy Functional Languages},
journal = {Information and Computation},
volume = {146},
number = {2},
pages = {100-137},
year = {1998},
issn = {0890-5401},
doi = {https://doi.org/10.1006/inco.1998.2735},
url = {https://www.sciencedirect.com/science/article/pii/S0890540198927353},
author = {G.W. Hamilton},
abstract = {If it can be determined at compile-time how many times values will be used within lazy functional programs, a number of useful optimisations can be performed. For example, call-by-need parameter passing can be converted to call-by-name, and in-place updating and compile-time garbage collection can be performed. In this paper, it is shown how this usage counting information can be obtained by static analysis. This analysis is not itself a major contribution of this paper; similar analyses have been defined before. The major contributions of this paper are that it provides a framework against which this analysis can be proved correct for a lazy functional language, and the analysis is proved to be correct with respect to this framework. The framework for proving the correctness of the analysis is provided by defining a store semantics which counts the number of times values are used.}
}

@article{park1991,
author = {Park, Young Gil and Goldberg, Benjamin},
title = {Reference Escape Analysis: Optimizing Reference Counting Based on the Lifetime of References},
year = {1991},
issue_date = {Sept. 1991},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {26},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/115866.115883},
doi = {10.1145/115866.115883},
journal = {SIGPLAN Not.},
month = {may},
pages = {178–189},
numpages = {12}
}

@inproceedings{mycroft1980,
author = {Mycroft, Alan},
title = {The Theory and Practice of Transforming Call-by-Need into Call-by-Value},
year = {1980},
isbn = {3540099816},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
booktitle = {Proceedings of the Fourth 'Colloque International Sur La Programmation' on International Symposium on Programming},
pages = {269–281},
numpages = {13}
}

@inproceedings{hudak1986,
author = {Hudak, Paul},
title = {A Semantic Model of Reference Counting and Its Abstraction (Detailed Summary)},
year = {1986},
isbn = {0897912004},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/319838.319876},
doi = {10.1145/319838.319876},
booktitle = {Proceedings of the 1986 ACM Conference on LISP and Functional Programming},
pages = {351–363},
numpages = {13},
location = {Cambridge, Massachusetts, USA},
series = {LFP '86}
}

@article{kaser1992,
author = {Kaser, O. and Pawagi, S. and Ramakrishnan, C. R. and Ramakrishnan, I. V. and Sekar, R. C.},
title = {Fast Parallel Implementation of Lazy Languages—the EQUALS Experience},
year = {1992},
issue_date = {Jan. 1992},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {V},
number = {1},
issn = {1045-3563},
url = {https://doi.org/10.1145/141478.141570},
doi = {10.1145/141478.141570},
abstract = {This paper describes EQUALS, a fast parallel implementation of a lazy functional language on a commercially available shared-memory parallel machine, the Sequent Symmetry.  In contrast to previous implementations, we detect parallelism automatically by propagating exhaustive (normal form) demand.  Another important difference between EQUALS and previous implementations is the use of reference counting for memory management instead of garbage collection.  Our implementation shows that reference counting leads to very good scalability, low memory requirements and improved locality.  We compare our results with sequntial SML/NJ as well as parallel (v, G-machine and GAML implementations.},
journal = {SIGPLAN Lisp Pointers},
month = {jan},
pages = {335–344},
numpages = {10}
}

@article{goldberg1989,
  title={Multiprocessor execution of functional programs},
  author={Benjamin Goldberg},
  journal={International Journal of Parallel Programming},
  year={1989},
  volume={17},
  pages={425-473},
  url={https://api.semanticscholar.org/CorpusID:27235482}
}

@article{barendsen1996,
  title={Uniqueness typing for functional languages with graph rewriting semantics},
  volume={6},
  DOI={10.1017/S0960129500070109},
  number={6},
  journal={Mathematical Structures in Computer Science},
  publisher={Cambridge University Press},
  author={Barendsen, Erik and Smetsers, Sjaak},
  year={1996},
  pages={579–612}
}

@book{pepels1988cyclic,
  title={A cyclic reference counting algorithm and its proof},
  author={Pepels, EJH and van Eekelen, MCJD and Plasmeijer, Marinus Jacobus},
  year={1988},
  publisher={Department of Theoretical Computer Science and Computational Models, Faculty~…}
}

@inproceedings{hausmann2015,
  title={The Agda UHC Backend},
  author={Philipp Hausmann},
  year={2015},
  url={https://api.semanticscholar.org/CorpusID:61450588}
}

@inproceedings{reynolds1972,
author = {Reynolds, John C.},
title = {Definitional Interpreters for Higher-Order Programming Languages},
year = {1972},
isbn = {9781450374927},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/800194.805852},
doi = {10.1145/800194.805852},
abstract = {Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language such as pure LISP). Examples include McCarthy's definition of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds' definitions of GEDANKEN, and recent unpublished work by L. Morris and C. Wadsworth. Such definitions can be classified according to whether the interpreter contains higher-order functions, and whether the order of application (i.e., call-by-value versus call-by-name) in the defined language depends upon the order of application in the defining language. As an example, we consider the definition of a simple applicative programming language by means of an interpreter written in a similar language. Definitions in each of the above classifications are derived from one another by informal but constructive methods. The treatment of imperative features such as jumps and assignment is also discussed.},
booktitle = {Proceedings of the ACM Annual Conference - Volume 2},
pages = {717–740},
numpages = {24},
keywords = {Reference, J-operator, Continuation, SECD machine, Lambda calculus, Closure, Programming language, PAL, Interpreter, Applicative language, LISP, Order of application, GEDANKEN, Language definition, Higher-order function},
location = {Boston, Massachusetts, USA},
series = {ACM '72}
}

@article{wadler1987,
author = {Wadler, Philip},
title = {Fixing some space leaks with a garbage collector},
journal = {Software: Practice and Experience},
volume = {17},
number = {9},
pages = {595-608},
keywords = {Space leak, Garbage collection, Functional languages, Lazy evaluation},
doi = {https://doi.org/10.1002/spe.4380170904},
url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/spe.4380170904},
eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1002/spe.4380170904},
abstract = {Abstract Some functional programs may use more space than would be expected. A modification to the garbage collector is suggested which solves this problem in some cases. Related work is discussed.},
year = {1987}
}

@inproceedings{augustsson1989,
author = {Augustsson, Lennart and Johnsson, Thomas},
title = {Parallel Graph Reduction with the (v , G)-Machine},
year = {1989},
isbn = {0897913280},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/99370.99386},
doi = {10.1145/99370.99386},
booktitle = {Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture},
pages = {202–213},
numpages = {12},
location = {Imperial College, London, United Kingdom},
series = {FPCA '89}
}

@inproceedings{augustsson1984,
author = {Augustsson, Lennart},
title = {A Compiler for Lazy ML},
year = {1984},
isbn = {0897911423},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/800055.802038},
doi = {10.1145/800055.802038},
abstract = {LML is a strongly typed, statically scoped functional Language with Lazy evaluation. It is compiled trough a number of program transformations which makes the code generation easier. Code is generated in two steps, first code for an abstract graph manipulation machine, the G-machine. From this code machine code is generated. Some benchmark tests are also presented.},
booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
pages = {218–227},
numpages = {10},
location = {Austin, Texas, USA},
series = {LFP '84}
}

@article{turner1979,
  title={A new implementation technique for applicative languages},
  author={David Turner},
  journal={Software: Practice and Experience},
  year={1979},
  volume={9},
  url={https://api.semanticscholar.org/CorpusID:40541269}
}

@inproceedings{wilson1992,
author = {Wilson, Paul R.},
title = {Uniprocessor Garbage Collection Techniques},
year = {1992},
isbn = {354055940X},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
booktitle = {Proceedings of the International Workshop on Memory Management},
pages = {1–42},
numpages = {42},
series = {IWMM '92}
}

@article{augustsson1998,
author = {Augustsson, Lennart},
title = {Cayenne—a Language with Dependent Types},
year = {1998},
issue_date = {Jan. 1999},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {34},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/291251.289451},
doi = {10.1145/291251.289451},
abstract = {Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts.Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.},
journal = {SIGPLAN Not.},
month = {sep},
pages = {239–250},
numpages = {12},
keywords = {dependent types, module systems, language design, type systems}
}

@inproceedings{10.1145/289423.289451,
author = {Augustsson, Lennart},
title = {Cayenne—a Language with Dependent Types},
year = {1998},
isbn = {1581130244},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/289423.289451},
doi = {10.1145/289423.289451},
abstract = {Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts.Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.},
booktitle = {Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming},
pages = {239–250},
numpages = {12},
keywords = {module systems, language design, dependent types, type systems},
location = {Baltimore, Maryland, USA},
series = {ICFP '98}
}

@InProceedings{vollmer2017,
  author =	{Vollmer, Michael and Spall, Sarah and Chamith, Buddhika and Sakka, Laith and Koparkar, Chaitanya and Kulkarni, Milind and Tobin-Hochstadt, Sam and Newton, Ryan R.},
  title =	{{Compiling Tree Transforms to Operate on Packed Representations}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{26:1--26:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.26},
  URN =		{urn:nbn:de:0030-drops-72737},
  doi =		{10.4230/LIPIcs.ECOOP.2017.26},
  annote =	{Keywords: compiler optimization, program transformation, tree traversal}
}

@InProceedings{demuijnckhughes2023,
  author =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  title =	{{Wiring Circuits Is Easy as \{0,1,\omega\}, or Is It...}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{8:1--8:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.8},
  URN =		{urn:nbn:de:0030-drops-182010},
  doi =		{10.4230/LIPIcs.ECOOP.2023.8},
  annote =	{Keywords: Hardware Design, Linear Types, Dependent Types, DSLs, Idris, SystemVerilog, Netlists}
}

@book{jones1987,
author = {Peyton Jones, Simon L.},
title = {The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science)},
year = {1987},
isbn = {013453333X},
publisher = {Prentice-Hall, Inc.},
address = {USA}
}


@article{goldberg1988,
title = "Multiprocessor execution of functional programs",
abstract = "Functional languages have recently gained attention as vehicles for programming in a concise and elegant manner. In addition, it has been suggested that functional programming provides a natural methodology for programming multiprocessor computers. This paper describes research that was performed to demonstrate that multiprocessor execution of functional programs on current multiprocessors is feasible, and results in a significant reduction in their execution times. Two implementations of the functional language ALFL were built on commercially available multiprocessors. Alfalfa is an implementation on the Intel iPSC hypercube multiprocessor, and Buckwheat is an implementation on the Encore Multimax shared-memory multiprocessor. Each implementation includes a compiler that performs automatic decomposition of ALFL programs and a run-time system that supports their execution. The compiler is responsible for detecting the inherent parallelism in a program, and decomposing the program into a collection of tasks, called serial combinators, that can be executed in parallel. The abstract machine model supported by Alfalfa and Buckwheat is called heterogeneous graph reduction, which is a hybrid of graph reduction and conventional stack-oriented execution. This model supports parallelism, lazy evaluation, and highe order functions while at the same time making efficient use of the processors in the system. The Alfalfa and Buckwheat runtime systems support dynamic load balancing, interprocessor communication (if required), and storage management. A large number of experiments were performed on Alfalfa and Buckwheat for a variety of programs. The results of these experiments, as well as the conclusions drawn from them, are presented.",
keywords = "Funtional languages, combinators, graph reduction, parallelism",
author = "Benjamin Goldberg",
year = "1988",
month = oct,
doi = "10.1007/BF01383883",
language = "English (US)",
volume = "17",
pages = "425--473",
journal = "International Journal of Parallel Programming",
issn = "0885-7458",
publisher = "Springer New York",
number = "5",

}
@inproceedings{lermen1986,
author = {Lermen, Claus-Werner and Maurer, Dieter},
title = {A Protocol for Distributed Reference Counting},
year = {1986},
isbn = {0897912004},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/319838.319875},
doi = {10.1145/319838.319875},
booktitle = {Proceedings of the 1986 ACM Conference on LISP and Functional Programming},
pages = {343–350},
numpages = {8},
location = {Cambridge, Massachusetts, USA},
series = {LFP '86}
}

@mastersthesis{turk2010,
  title={A modern back-end for a dependently-typed language},
  author={Turk, Remi},
  year={2010},
  school={Universiteit van Amsterdam},
  url={https://eprints.illc.uva.nl/id/document/1982}
}
@inproceedings{cockx2022,
author = {Cockx, Jesper and Melkonian, Orestis and Escot, Lucas and Chapman, James and Norell, Ulf},
title = {Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs},
year = {2022},
isbn = {9781450394383},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3546189.3549920},
doi = {10.1145/3546189.3549920},
abstract = {Modern dependently typed languages such as Agda can be used to  
 statically enforce the correctness of programs. However, they still  
 lack the large ecosystem of a more popular language like Haskell.  
 To combine the strength of both approaches, we present agda2hs, a  
 tool that translates an expressive subset of Agda to readable  
 Haskell, erasing dependent types and proofs in the process.  
 Thanks to Agda's support for erasure annotations, this  
 process is both safe and transparent to the user.  
 Compared to other tools for program extraction, agda2hs uses a syntax  
 that is already familiar to functional programmers, allows for both  
 intrinsic and extrinsic approaches to verification, and produces  
 Haskell code that is easy to read and audit by programmers with no  
 knowledge of Agda.  

 We present a practical use case of agda2hs at IOG  
 to verify properties of a program generator.  
 While both agda2hs and its ecosystem are still young, our  
 experiences so far show that this is a viable approach to make  
 verified functional programming available to a broader audience.  

 This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked.},
booktitle = {Proceedings of the 15th ACM SIGPLAN International Haskell Symposium},
pages = {108–122},
numpages = {15},
keywords = {Agda, Dependent types, Formal verification, Program extraction},
location = {Ljubljana, Slovenia},
series = {Haskell 2022}
}

@InProceedings{lam2024,
author="Lam, Chun Kit
and Parreaux, Lionel",
editor="Gibbons, Jeremy
and Miller, Dale",
title="Being Lazy When It Counts",
booktitle="Functional and Logic Programming",
year="2024",
publisher="Springer Nature Singapore",
address="Singapore",
pages="188--216",
abstract="Functional programming (FP) lets users focus on the business logic of their applications by providing them with high-level and composable abstractions. However, both automatic memory management schemes traditionally used for FP, namely tracing garbage collection and reference counting, may introduce latencies in places that can be hard to predict, which limits the applicability of the FP paradigm.",
isbn="978-981-97-2300-3"
}