The concept of a supercompiler

DOI10.1145/5956.5957zbMath0598.68016OpenAlexW2020024606WikidataQ30040121 ScholiaQ30040121MaRDI QIDQ3732942

Valentin Turchin

Publication date: 1986

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: http://www.acm.org/pubs/contents/journals/toplas/1986-8/

zbMATH Keywords

lazy evaluationprogram transformationredundancypartial evaluationdrivingPrologcontrol transferprogram transformerequivalence rulesmetasystem transitionRefal

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (39)

A regeneration scheme for generating extensions ⋮ Verification as a parameterized testing (experiments with the SCP4 supercompiler) ⋮ Proving properties of functional programs by equality saturation ⋮ Supercompilation for Martin-Lof's type theory ⋮ Rewriting techniques for program synthesis ⋮ Inductive Prover Based on Equality Saturation for a Lazy Functional Language ⋮ Asymptotic Speedups, Bisimulation and Distillation (Work in Progress) ⋮ Certifying Supercompilation for Martin-Löf’s Type Theory ⋮ Annotated bibliography on partial evaluation and mixed computation ⋮ On the transformation of logic programs with instantiation based computation rules ⋮ Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic ⋮ Horn Clause Solvers for Program Verification ⋮ The next 700 program transformers ⋮ Excommunication: transforming \(\pi \)-calculus specifications to remove internal communication ⋮ Closed-form upper bounds in static cost analysis ⋮ A positive supercompiler ⋮ Reverse universal resolving algorithm and inverse driving ⋮ REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Static semantics, types, and binding time analysis ⋮ Proving the correctness of recursion-based automatic program transformations ⋮ Polynomial-time inverse computation for accumulative functions with multiple data traversals ⋮ On one application of computations with oracle ⋮ Higher-level supercompilation as a metasystem transition ⋮ The narrowing-driven approach to functional logic program specialization ⋮ Program transformation system based on generalized partial computation ⋮ Interleaving Symbolic Execution and Partial Evaluation ⋮ Ping-pong protocols as prefix grammars: modelling and verification via program transformation ⋮ Proving the correctness of recursion-based automatic program transformations ⋮ Refal ⋮ An improved reductant calculus using fuzzy partial evaluation techniques ⋮ Unnamed Item ⋮ Extending a partial evaluator which supports separate compilation ⋮ FROM STANDARD TO NON-STANDARD SEMANTICS BY SEMANTICS MODIFIERS ⋮ Constraint-based partial evaluation for imperative languages ⋮ Essence of generalized partial computation ⋮ Reflection in conditional rewriting logic ⋮ Derivation of efficient logic programs by specialization and reduction of nondeterminism

This page was built for publication: The concept of a supercompiler