Supercompilation is a principiled program transformation technique that symbolically evaluates a given input program into its more efficient version, eliminating as much of computational overhead as possible. From a given program it builds a process graph of dynamically encountered configurations (expressions with unknown variables), converts loops into special edges between the configurations, & finally residualizes the process graph into a structurally simpler output program in the same or different language. Furthermore, with suitable extensions it can achieve asymptotic speedups for some functional algorithms.
This is a collection of resources for studying supercompilation & its applications, ranging from introductory materials to advanced papers. Any questions regarding supercompilation will be welcomed in the issues.
- SPSC -- A Small Positive Supercompiler in Scala, Haskell, Python, Ruby, JavaScript & Idris.
- HOSC -- A higher-order call-by-name supercompiler for a subset of Haskell.
- JSCP -- A supercompiler for the Java programming language.
- MRSC -- A toolkit for rapid design and prototyping of (multi-result) supercompilers.
- TT-Lite -- A supercompiler for a version of Martin-Löf’s Type Theory (MLTT).
- sc-mini -- A minimal positive supercompiler written in Haskell.
- erlscp -- A supercompiler pass for the Erlang programming language.
- agda-simple-scp -- A simple supercompiler formally verified in Agda.
- Mazeppa -- A modern supercompiler for call-by-value functional languages.
- Distiller -- The implementation of the distillation algorithm.
- Turchin, Valentin F. "The concept of a supercompiler." ACM Transactions on Programming Languages and Systems (TOPLAS) 8.3 (1986): 292-325.
$${\textbf{\color{orange}must read}}$$ $${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{gold}popular}}$$ $${\textbf{\color{cyan}Refal}}$$
URL, webarchive
- Glück, Robert, and Andrei V. Klimov. "Occam's razor in metacomputation: the notion of a perfect process tree." International Workshop on Static Analysis. Berlin, Heidelberg: Springer Berlin Heidelberg, 1993.
$${\textbf{\color{orange}must read}}$$
URL, webarchive - Turchin, Valentin F. "Program transformation with metasystem transitions." Journal of Functional Programming 3.3 (1993): 283-313.
$${\textbf{\color{cyan}Refal}}$$
URL, webarchive
- Turchin, V., and A. Nemytykh. Metavariables: Their implementation and use in Program Transformation. CCNY Technical Report CSc TR-95-012, 1995.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{cyan}Refal}}$$
URL, webarchive - Sørensen, Morten Heine, and Robert Glück. "An Algorithm of Generalization in Positive Supercompilation." ILPS. Vol. 95. 1995.
$${\textbf{\color{gold}popular}}$$
URL, webarchive
- Soerensen, Morten Heine, Robert Glück, and Neil D. Jones. "A positive supercompiler." Journal of functional programming 6.6 (1996): 811-838.
$${\textbf{\color{lightgreen}introductory}}$$ $${\textbf{\color{gold}popular}}$$
URL, webarchive - Glück, Robert, and Morten Heine Sørensen. "A roadmap to metacomputation by supercompilation." Partial Evaluation: International Seminar Dagstuhl Castle, Germany, February 12–16, 1996 Selected Papers. Springer Berlin Heidelberg, 1996.
$${\textbf{\color{lightgreen}introductory}}$$ $${\textbf{\color{violet}inspirational}}$$
URL, webarchive - Turchin, Valentin F. "Metacomputation: MST plus SCP." Proc. of the Dagstuhl Seminar on Partial Evaluation, Springer-Verlag. 1996.
$${\textbf{\color{cyan}Refal}}$$
URL, webarchive - Nemytykh, Andrei P., Victoria A. Pinchuk, and Valentin F. Turchin. "A self-applicable supercompiler." Partial Evaluation: International Seminar Dagstuhl Castle, Germany, February 12–16, 1996 Selected Papers. Springer Berlin Heidelberg, 1996.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{cyan}Refal}}$$
URL, webarchive - Turchin, Valentin F. "Supercompilation: Techniques and results." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 1996.
$${\textbf{\color{cyan}Refal}}$$
URL, webarchive - Turchin, Valentin F. "On generalization of lists and strings in supercompilation." Technical Report CSc. TR 96-002 (1996).
$${\textbf{\color{cyan}Refal}}$$
URL, webarchive
- Sørensen, Morten Heine B. "Convergence of program transformers in the metric space of trees." International Conference on Mathematics of Program Construction. Berlin, Heidelberg: Springer Berlin Heidelberg, 1998.
$${\textbf{\color{orange}must read}}$$
URL, webarchive - Sørensen, Morten Heine B., and Robert Glück. "Introduction to supercompilation." DIKU International Summer School. Berlin, Heidelberg: Springer Berlin Heidelberg, 1998. 246-270.
$${\textbf{\color{lightgreen}introductory}}$$
URL, webarchive
- Secher, Jens Peter, and Morten Heine Sørensen. "On perfect supercompilation." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999.
URL, webarchive
- Secher, Jens Peter. "Driving in the jungle." Symposium on Program as Data Objects. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Abramov, Sergei, and Robert Glück. "From standard to non-standard semantics by semantics modifiers." International Journal of Foundations of Computer Science 12.02 (2001): 171-211.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive
- Korlyukov, A. V., and Andrei P. Nemytykh. "Supercompilation of Double Interpretation. (How One Hour of the Machine’s Time Can Be Turned to One Second)." 2002
$${\textbf{\color{violet}inspirational}}$$
URL, webarchive
- Klimov, Andrei Valentinovich. "A program specialization relation based on supercompilation and its properties." Препринты Института прикладной математики им. МВ Келдыша РАН 0 (2008): 26-28.
URL, webarchive - Klimov, Andrei V. "An approach to supercompilation for object-oriented languages: the Java Supercompiler case study." Nemytykh [28] (2008): 43-53.
$${\textbf{\color{lightblue}practical}}$$
URL, webarchive - Lisitsa, Alexei, and Andrei P. Nemytykh. "Reachability analysis in verification via supercompilation." International Journal of Foundations of Computer Science 19.04 (2008): 953-969.
$${\textbf{\color{lightblue}practical}}$$
URL, webarchive - Lisitsa, Alexei, and Matt Webster. "Supercompilation for equivalence testing in metamorphic computer viruses detection." Proceedings of the First International Workshop on Metacomputation in Russia. Vol. 226. 2008.
$${\textbf{\color{lightblue}practical}}$$
URL, webarchive - Lisitsa, Alexei, and Andrei P. Nemytykh. "Extracting bugs from the failed proofs in verification via supercompilation." Tests and Proofs: Papers Presented at the Second International Conference TAP. No. 5. 2008.
$${\textbf{\color{lightblue}practical}}$$
URL
- Jonsson, Peter A., and Johan Nordlander. "Positive supercompilation for a higher order call-by-value language." ACM SIGPLAN Notices 44.1 (2009): 277-288.
$${\textbf{\color{gold}popular}}$$
URL - Klyuchnikov, Ilya, and Sergei Romanenko. "Proving the equivalence of higher-order terms by means of supercompilation." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009.
URL, webarchive - Klyuchnikov, Ilya, and Sergei Romanenko. "SPSC: a simple supercompiler in Scala." PU 9 (2009): 5.
$${\textbf{\color{pink}implementation}}$$
URL, webarchive - Reich, Jason S. Optimus Prime: A new tool for interactive transformation and supercompilation of functional programs. Diss. Masters dissertation, University of York, UK, 2009.
$${\textbf{\color{pink}implementation}}$$
URL - Klimov, Andrei V. "A Java supercompiler and its application to verification of cache-coherence protocols." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009.
$${\textbf{\color{lightblue}practical}}$$
URL
- Bolingbroke, Maximilian, and Simon Peyton Jones. "Supercompilation by evaluation." Proceedings of the third ACM Haskell symposium on Haskell. 2010.
$${\textbf{\color{pink}implementation}}$$ $${\textbf{\color{gold}popular}}$$ $${\textbf{\color{lightgreen}introductory}}$$
URL - Jonsson, Peter, and Johan Nordlander. "Strengthening supercompilation for call-by-value languages." International Valentin Turchin Memorial Workshop on Metacomputation in Russia: 01/07/2010-05/07/2010. Ailamazyan University of Pereslavl, 2010.
URL, webarchive - Klyuchnikov, Ilya, and Sergei Romanenko. "Towards higher-level supercompilation." Second International Workshop on Metacomputation in Russia. Vol. 2. No. 4.2. 2010.
URL - Klyuchnikov, Ilya Grigorievich. "Supercompiler HOSC 1.5: homeomorphic embedding and generalization in a higher-order setting." Keldysh Institute Preprints 62 (2010): 1-23.
URL, webarchive - Mitchell, Neil. "Rethinking supercompilation." ACM Sigplan Notices 45.9 (2010): 309-320.
$${\textbf{\color{pink}implementation}}$$ $${\textbf{\color{violet}inspirational}}$$
URL - Klyuchnikov, Ilya Grigorievich. "Towards effective two-level supercompilation." Препринты Института прикладной математики им. МВ Келдыша РАН 0 (2010): 81-28.
URL, webarchive
- Hamilton, Geoff W., and Neil D. Jones. "Proving the correctness of unfold/fold program transformations using bisimulation." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011.
URL - Jonsson, Peter A., and Johan Nordlander. "Taming code explosion in supercompilation." Proceedings of the 20th ACM SIGPLAN workshop on Partial evaluation and program manipulation. 2011.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{crimson}advanced}}$$
URL - Jonsson, Peter A. Time-and size-efficient supercompilation. Diss. Luleå tekniska universitet, 2011.
URL, webarchive - Klyuchnikov, Ilya, and Sergei A. Romanenko. "Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011.
URL, webarchive - Bolingbroke, Maximilian, and Simon Peyton Jones. "Improving supercompilation: tag-bags, rollback, speculation, normalisation, and generalisation." ICFP. (2011).
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive
- Grechanik, Sergei A. "Overgraph representation for multi-result supercompilation." Proceedings of the Third International Valentin Turchin Workshop on Metacomputation. Pereslavl-Zalessky: Ailamazyan University of Pereslavl, 2012.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Klyuchnikov, Ilya G., and Sergei A. Romanenko. "Formalizing and implementing multi-result supercompilation." Klimov and Romanenko [18] (2012): 142-164.
URL - Klimov, Andrei V., Ilya G. Klyuchnikov, and Sergei A. Romanenko. "Automatic verification of counter systems via domain-specific multi-result supercompilation." Preprint 19 (2012): 2012-19.
URL, webarchive
- Hamilton, G. W. "On the Termination of Higher-Order Positive Supercompilation." Proc. of the First International Workshop on Verification and Program Transformation. 2013.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Grechanik, Sergei Aleksandrovich. "Supercompilation by hypergraph transformation." Препринты Института прикладной математики им. МВ Келдыша РАН 0 (2013): 26-24.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Bolingbroke, Maximilian C. Call-by-need supercompilation. No. UCAM-CL-TR-835. University of Cambridge, Computer Laboratory, 2013.
$${\textbf{\color{gold}popular}}$$
URL, webarchive
- Klyuchnikov, Ilya, and Dimitur Krustev. "Supercompilation: Ideas and methods." The Monad. Reader Issue 23 (2014): 17.
$${\textbf{\color{pink}implementation}}$$ $${\textbf{\color{lightgreen}introductory}}$$
URL, webarchive - Mogensen, Torben Ægidius. "Supercompilation for Datatypes." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014.
$${\textbf{\color{violet}inspirational}}$$
URL, webarchive - Klyuchnikov, Ilya, and Sergei Romanenko. "Certifying supercompilation for Martin-Löf’s type theory." International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Grechanik, Sergei, Ilya Klyuchnikov, and Sergei Romanenko. "Staged multi-result supercompilation: Filtering by transformation." Proceedings of the Fourth International Valentin Turchin Workshop on Metacomputation/ed. by A. Klimov, S. Romanenko.—Pereslavl-Zalessky, Russia: Pereslavl Zalessky: Publishing House” University of Pereslavl. 2014.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive
- Klyuchnikov, Ilya G., and Sergei A. Romanenko. "Supercompilation for Martin-Lof’s type theory." Programming and Computer Software 41 (2015): 170-182.
URL, webarchive
- Glück, Robert, Andrei Klimov, and Antonina Nepeivoda. "Nonlinear Configurations for Superlinear Speedup by Supercompilation." Fifth International Valentin Turchin Workshop on Metacomputation. 2016.
$${\textbf{\color{violet}inspirational}}$$
URL, webarchive - Grechanik, Sergei. "Towards Unification of Supercompilation and Equality Saturation." Proceedings of the Fifth International Valentin Turchin Workshop on Metacomputation/ed. by A. Klimov, S. Romanenko.—Pereslavl-Zalessky, Russia: Pereslavl Zalessky: Publishing House” University of Pereslavl. 2016.
$${\textbf{\color{crimson}advanced}}$$
URL, webarchive
- Nystrom, Nathaniel. "A scala framework for supercompilation." Proceedings of the 8th ACM SIGPLAN International Symposium on Scala. 2017.
URL
- Климов, Андрей Валентинович, and Сергей Анатольевич Романенко. "Суперкомпиляция: основные принципы и базовые понятия." Препринты Института прикладной математики им. МВ Келдыша РАН 0 (2018): 111-36.
$${\textbf{\color{lightgreen}introductory}}$$
URL, webarchive - Романенко, Сергей Анатольевич. "Суперкомпиляция: гомеоморфное вложение, вызов по имени, частичные вычисления." Препринты ИПМ им. МВ Келдыша 209 (2018): 1-32.
$${\textbf{\color{lightgreen}introductory}}$$
URL, webarchive
- Krustev, Dimitur Nikolaev. "Optimizing Program Size Using Multi-result Supercompilation." arXiv preprint arXiv:2008.04669 (2020).
URL, webarchive
- Klimov, A. V. "Supercompilation and partial evaluation are still not widely used in practice. Why and what to do?." Scientific Services & Internet. Vol. 24. 2022.
URL, webarchive
- Leuschel, Michael. "Homeomorphic embedding for online termination of symbolic methods." The essence of computation: complexity, analysis, transformation. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002. 379-403.
$${\textbf{\color{lightgreen}introductory}}$$
URL, webarchive - Nash-Williams, C. St JA. "On well-quasi-ordering finite trees." Mathematical Proceedings of the Cambridge Philosophical Society. Vol. 59. No. 4. Cambridge University Press, 1963.
URL, webarchive - Bolingbroke, Maximilian, Simon Peyton Jones, and Dimitrios Vytiniotis. "Termination combinators forever." Proceedings of the 4th ACM symposium on Haskell. 2011.
$${\textbf{\color{violet}inspirational}}$$
URL, webarchive
- Hamilton, Geoffrey William, and Neil D. Jones. "Distillation with labelled transition systems." Proceedings of the ACM SIGPLAN 2012 workshop on Partial Evaluation and Program Manipulation. 2012.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{crimson}advanced}}$$
URL - Hamilton, Geoff. "The Next 700 Program Transformers." International Symposium on Logic-Based Program Synthesis and Transformation. Cham: Springer International Publishing, 2021.
$${\textbf{\color{violet}inspirational}}$$ $${\textbf{\color{crimson}advanced}}$$
URL, webarchive - Hamilton, Geoff W. "Poítin: Distilling theorems from conjectures." Electronic Notes in Theoretical Computer Science 151.1 (2006): 143-160.
URL - Hamilton, Geoff W., and M. H. Kabir. "Constructing programs from metasystem transition proofs." (2008).
URL, webarchive - Mendel-Gleason, Gavin E., and Geoff W. Hamilton. "Supercompilation and normalisation by evaluation." (2010).
URL, webarchive - Jones, Neil D., and Geoff W. Hamilton. "Superlinear speedup by program transformation." Third International Valentin Turchin Workshop on Metacomputation. 2012.
URL, webarchive