Abstract Catamorphisms are functions that are recursively defined on list and trees and, in general, on algebraic data types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of constrained Horn clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a nontrivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.

This paper presents some ideas concerning program manipulation and program transformation from the early days of their development. Particular emphasis will be given to program transformation techniques in the area of functional programming and constraint logic programming. We will also indicate current applications of program transformation techniques to the verification of program properties and program synthesis.

Abstract We address the problem of checking the satisfiability of constrained Horn clauses (CHCs) defined on algebraic data types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the arguments of the predicates have only basic types, such as integers and booleans. Thus, our technique avoids, during satisfiability checking, the explicit use of proof rules based on induction over the ADTs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates, whose definitions correspond to lemmas that are used when making inductive proofs. We present an algorithm that performs the automatic removal of ADTs by applying the new rule, together with the traditional folding/unfolding rules. We prove that, under suitable hypotheses, the set of the transformed clauses is satisfiable if and only if so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal. We also show that our approach is competitive with respect to tools that extend CHC solvers with the use of inductive rules.

Abstract This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.

Abstract We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on constrained Horn clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate algebraic data types (ADTs) and a class of contracts specified by catamorphisms, that is, functions defined by simple recursion schemata on the given ADTs. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. To overcome this difficulty, we propose a transformation technique that removes the ADT terms from CHCs and derives new sets of clauses that work on basic sorts only, such as integers and booleans. Thus, when using the derived CHCs there is no need for induction rules on ADTs. We prove that the transformation is sound, that is, if the derived set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts for ADT manipulating programs.

We present an operational semantics for time-aware business processes, that is, processes modeling the execution of business activities, whose durations are subject to linear constraints over the integers. We assume that some of the durations are controllable, that is, they can be determined by the organization that executes the process, while others are uncontrollable, that is, they are determined by the external world. Then, we consider controllability properties, which guarantee the completion of the execution of the process, satisfying the given duration constraints, independently of the values of the uncontrollable durations. Controllability properties are encoded by quantified reachability formulas, where the reachability predicate is recursively defined by means of constrained Horn clauses (CHCs). These clauses are automatically derived from the operational semantics of the process. Finally, we present two algorithms for solving the so called weak and strong controllability problems. Our algorithms reduce these problems to the verification of a set of quantified integer constraints, which are simpler than the original quantified reachability formulas, and can effectively be handled by state-of-the-art CHC solvers.

LogicaComputazionale, CILC 2016) that was hosted by the Università degli Studi di Milano-Bicocca, Italy, from June 20th to June 22th, 2016.The event was the thirty-first edition of the annual meeting of the Italian Association for Logic Programming (GULP, Gruppo Ricercatori e Utenti di Logic Programming).Since its first edition, the annual conference organized by GULP is the main occasion of meeting and exchanging ideas and experiences among Italian researchers who work in the field of Computational Logic.During the years, this meeting has extended its horizons from the area of Logic Programming to the area of Computational Logic in general, including aspects of Artificial Intelligence and Deductive Databases.The program of CILC 2016 included 21 technical papers accepted for presentation and a few demos.Paper selection was made by peer reviewing.vi iii Description Logic ALC based on the combination of a typicality operator and the well-established non-monotonic mechanism of rational closure, which allows one to deal with prototypical properties and defeasible inheritance.Martin Sticht presents a multi-agent version of dialogical logic that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones, which are related to two-player dialogues.We would like to thank the Department of Computer

Abstract It is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based onpredicate abstractionare sometimes unable to verify satisfiability because they look for models that are definable in a given class 𝓐 of constraints, called 𝓐-definable models. We introduce a transformation technique, calledPredicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an 𝓐-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on 𝓐, the unfold/fold transformation rules preserve the existence of an 𝓐-definable model, that is, if the original clauses have an 𝓐-definable model, then the transformed clauses have an 𝓐-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an 𝓐-definable modelif and only ifthe original ones have an 𝓐-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for 𝓐-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an 𝓐-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification ofrelational properties of programs, that is, properties relating two programs (such as program equivalence) or two executions of the same program (such as non-interference). Finally, we perform an experimental evaluation of the proposed techniques to assess the effectiveness of Predicate Pairing in increasing the power of CHC solving.

Abstract We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists and trees. We propose a transformation technique whose objective is the removal of these data structures from CHCs, hence reducing their satisfiability to a satisfiability problem for CHCs on integers and booleans. We propose a transformation algorithm and identify a class of clauses where it always succeeds. We also consider an extension of that algorithm, which combines clause transformation with reasoning on integer constraints. Via an experimental evaluation we show that our technique greatly improves the effectiveness of applying the Z3 solver to CHCs. We also show that our verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrec t defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

This special issue of Fundamenta Informaticae contains the revised, extended versions of selected papers presented at the Italian Conference on Computational Logic (Convegno Italiano di Logica Computazionale, CILC 2014) which was hosted by the University of Turin, Italy, from June 16th to June 18th, 2014.The event was the twenty-ninth edition of the annual meeting of the Italian Association for Logic Programming (GULP, Gruppo Ricercatori e Utenti di Logic Programming).Since its first edition, which took place in Genoa in 1986, the annual conference organized by GULP is the main occasion of meeting and exchanging ideas and experiences among Italian researchers who work in the field of Computational Logic.During the years, this annual meeting extended its horizons from the specific field of traditional Logic Programming to more general declarative programming as well as to Artificial Intelligence and Deductive Databases.All these areas had a very significant growth over the last decades and nowadays they all play a crucial role in the fields of Information Processing and Computer Science.The program of CILC 2014 included 29 technical papers accepted for presentation (23 for long presentation and 6 for short presentation).Paper selection was made by peer reviewing.The technical presentations were of high quality and concerned several topics related to computational logic, including probabilistic logic programming, verification of logic programs, answer set programming, revision and query of ontologies, argumentation theory, proof and decision systems for non-classical logics, computable set theory, multi-agent systems, and machine learning.The conference program included also two invited talks: (i) "From logic programming to argumentation and back", by Francesca Toni (Department of Computing, Imperial College London, U.K.), and (ii) "Tractable approaches to consistent query answering in ontology-based-data access", by Riccardo Rosati (DIAG, Dipartimento di Ingegneria informatica, automatica e gestionale, Università di Roma "Sapienza", Italy).Some of the papers presented at the conference were selected for this special issue and their authors were invited to submit an improved, extended version for publication.The papers that have been accepted went through a two-round careful review by qualified international referees, to whom we express our deep gratitude for their comments and criticisms.

We present a method for automatically generating verification conditions for a class of imperative programs and safety properties. Our method is parametric with respect to the semantics of the imperative programming language, as it specializes, by using unfold/fold transformation rules, a Horn clause interpreter that encodes that semantics.

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ} prog {ψ} that defines a par tial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

Abstract We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a programprog, we consider a partial correctness specification of the form {ϕ},prog{ψ}, where the assertions ϕ and ψ are predicates defined by a setSpecof possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also calledconstrained Horn clauses). The verification method consists in constructing a setPCof constrained Horn clauses whose satisfiability implies that {ϕ},prog, {ψ} is valid. We highlight some limitations of state-of-the-art constrained Horn clause solving methods, here calledLA-solving methods, which prove the satisfiability of the clauses by looking for linear arithmetic interpretations of the predicates. In particular, we prove that there exist some specifications that cannot be proved valid by any of thoseLA-solving methods. These specifications require the proof of satisfiability of a setPCof constrained Horn clauses that containnonlinear clauses(that is, clauses with more than one atom in their premise). Then, we present a transformation, calledlinearization, that convertsPCinto a set oflinearclauses (that is, clauses with at most one atom in their premise). We show that several specifications that could not be proved valid byLA-solving methods, can be proved valid after linearization. We also present a strategy for performing linearization in an automatic way and we report on some experimental results obtained by using a preliminary implementation of our method.

We present a method for verifying properties of imperative programs by using techniques based on the specialization of constraint logic programs (CLP). We consider a class of C programs with integer variables and we focus our attention on safety properties, stating that no error configuration can be reached from the initial configurations. We encode the interpreter of the language as a CLP program I, and we also encode the safety property to be verified as the negation of a predicate unsafe defined in I. Then, we specialize the CLP program I with respect to the given C program and the given initial and error configurations, with the objective of deriving a new CLP program I_sp which either contains the fact 'unsafe' (and in this case the C program is proved unsafe) or contains no clauses with head 'unsafe' (and in this case the C program is proved safe). If I_sp does not enjoy this property we iterate the specialization process with the objective of deriving a CLP program where we can prove unsafety or safety. During the various specializations we may apply different strategies for propagating information (either propagating forward from an initial configuration, or propagating backward from an error configuration) and different operators (such as widening and convex hull operators) for generalizing predicate definitions. Due to the undecidability of program safety, the iterated specialization process may not terminate. By an experimental evaluation carried out on a set of examples taken from the literature, we show that our method is competitive with respect to state-of-the-art software model checkers.

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise.

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

This special issue of Fundamenta Informaticae contains the revised, extended versions of selected papers presented at the Italian Conference on Computational Logic (Convegno Italiano di Logica Computazionale, CILC 2011) which was held at the University "G.d'Annunzio" of Chieti-Pescara, Italy.This conference was the twenty-sixth edition of the annual meeting organized by the Italian Association for Logic Programming (GULP, Gruppo Ricercatori e Utenti di Logic Programming), which, since its first edition in 1986, constitutes the main Italian forum for researchers, users, and developers to discuss work and exchange ideas on Computational Logic and related areas, such as Artificial Intelligence and Deductive Databases.All these areas had a very significant growth over the last decades and nowadays they all play a crucial role in the fields of Information Processing and Computer Science.The program of the CILC 2011 conference featured thirty papers (twenty-one which had a long presentation and nine which had a short presentation), two invited talks: (i) one by A. Omicini (University of Bologna) on: "Coordination Models and Technologies toward Self-Organising Systems", and (ii) one by F. Spoto (University of Verona) on: "Static Analysis of Java.Can we be logical?", and a tutorial by F. Riguzzi (University of Ferrara) on: "Probabilistic Logic Languages".The quality of the technical contributions and the number of participants (about fifty, most of whom were young researchers) confirm that the Italian Computational Logic community is very lively and active.Some of the presented papers were selected and their authors were invited to submit an improved version for publication in this special issue.The papers accepted in this issue passed two rounds of careful reviews by qualified international referees, to whom we express our deep gratitude for their comments which helped the authors to improve the quality of their papers.

Abstract We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.

Abstract Many approaches proposed in the literature for proving the correctness of unfold/fold transformations of logic programs make use of measures associated with program clauses. When from a program P 1 we derive a program P 2 by applying a sequence of transformations, suitable conditions on the measures of the clauses in P 2 guarantee that the transformation of P 1 into P 2 is correct, that is, P 1 and P 2 have the same least Herbrand model. In the approaches proposed so far, clause measures are fixed in advance, independently of the transformations to be proved correct. In this paper we propose a method for the automatic generation of clause measures which, instead, takes into account the particular program transformation at hand. During the application of a sequence of transformations we construct a system of linear equalities and inequalities over nonnegative integers whose unknowns are the clause measures to be found, and the correctness of the transformation is guaranteed by the satisfiability of that system. Through some examples we show that our method is more powerful and practical than other methods proposed in the literature. In particular, we are able to establish in a fully automatic way the correctness of program transformations which, by using other methods, are proved correct at the expense of fixing in advance sophisticated clause measures.

We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). Every concurrent program to be synthesized is specified by providing both the behavioural and the structural properties

We consider infinite state reactive systems specified by using linear constraints over the integers, and we address the problem of verifying safety properties of these systems by applying reachability analysis techniques. We propose a method based on

Theory and experimentation are two roots common to many scientific disciplines such as Physics, Medicine, and Computer Science. In all these disciplines theory and experimentation are tightly intertwined: they grow together and together make Science progress and evolve.

This special issue of Fundamenta Informaticae contains the revised, extended versions of selected \npapers presented at the Italian Conference on Computational Logic (Convegno Italiano di Logica Com- \nputazionale, CILC’09) which was held at the Engineering Department of the University of Ferrara, Italy.

Abstract We consider an extension of logic programs, called ω-programs, that can be used to define predicates overinfinite lists. ω-programs allow us to specify properties of the infinite behavior of reactive systems and, in general, properties of infinite sequences of events. The semantics of ω-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming ω-programs. We show that these new rules are correct, that is, their application preserves the perfect model semantics. Then we outline a general methodology based on program transformation for verifying properties of ω-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Büchi automata and ω-regular languages.

The existential variables of a clause in a constraint logic program \nare the variables which occur in the body of the clause and not in \nits head. The elimination of these variables is a transformation \ntechnique which is often used for improving program efficiency and \nverifying program properties. We consider a folding transformation \nrule which ensures the elimination of existential variables and we \npropose an algorithm for applying this rule in the case where the \nconstraints are linear inequations over rational or real numbers. \nThe algorithm combines techniques for matching terms modulo \nequational theories and techniques for solving systems of linear \ninequations. Through some examples we show that an implementation of \nour folding algorithm has a good performance in practice.

We address the problem of proving total correctness of transformation rules for definite logic programs. We consider a general transformation rule, called clause replacement, which consists in transforming a program P into a new program Q by replacing a set Γ1 of clauses occurring in P by a new set Γ2 of clauses, provided that Γ1 and Γ2 are equivalent in the least Herbrand model M(P) of the program P.We propose a general method for proving that clause replacement is totally correct, that is, M(P)=M(Q). Our method consists in showing that the transformation of P into Q can be performed by: (i) adding extra arguments to predicates, thereby constructing from the given program P an annotated program α(P), (ii) applying clause replacements and transforming the annotated program α(P) into a terminating annotated program β(Q, and (iii) erasing the annotations from β(Q), thereby getting Q.Our method does not require that either P or Q terminates and it is parametric w.r.t. the annotations. By providing different definitions for these annotations, we can easily prove the total correctness of many versions of the unfolding, folding, and goal replacement rules proposed in the literature.

We consider a simple extension of logic programming where variables may range over goals and goals may be arguments of predicates. In this language we can write logic programs which use goals as data. We give practical evidence that, by exploiting this capability when transforming programs, we can improve program efficiency. We propose a set of program transformation rules which extend the familiar unfolding and folding rules and allow us to manipulate clauses with goals which occur as arguments of predicates. In order to prove the correctness of these transformation rules, we formally define the operational semantics of our extended logic programming language. This semantics is a simple variant of LD-resolution. When suitable conditions are satisfied this semantics agrees with LD-resolution and, thus, the programs written in our extended language can be run by ordinary Prolog systems. Our transformation rules are shown to preserve the operational semantics and termination.

Abstract. We present a new program transformation strategy based on the introduction of lists. This strategy is an extension of the tupling strategy which is based on the introduction of tuples of fixed length. The list introduction strategy overcomes some of the limitations of the tupling strategy and, in particular, it makes it possible to transform general recursive programs into linear recursive ones also in cases when this transformation cannot be performed by the tupling strategy. The linear recursive programs we derive by applying the list introduction strategy have in most cases very good time and space performance because they avoid repeated evaluations of goals and unnecessary constructions of data structures.

Program specialization is a collection of program transformation techniques for improving program efficiency by exploiting some information available at compile-time about the input data. We show that current techniques for program specialization based on partial evaluation do not perform well on nondeterministic logic programs. We then consider a set of transformation rules which extend the ones used for partial evaluation, and we propose a strategy to direct the application of these extended rules so to derive very efficient specialized programs. The efficiency improvements which may even be exponential, are achieved because the derived programs are semi-deterministic and the operations which are performed by the initial programs in different branches of the computation trees, are performed in the specialized programs within single branches. We also make use of mode information to guide the unfolding process and to reduce nondeterminism. To exemplify our technique, we show that we can automatically derive very efficient semi-deterministic matching programs and semi-deterministic parsers for regular languages. The derivations we have performed could not have been done by previously known partial evaluation techniques.

article Semantics preserving transformation rules for Prolog Share on Authors: Maurizio Proietti IASI-CNR, Viale Manzoni 30, 00185 Roma, Italy IASI-CNR, Viale Manzoni 30, 00185 Roma, ItalyView Profile , Alberto Pettorossi Electronics Department, University of Rome II, 00173 Roma, Italy Electronics Department, University of Rome II, 00173 Roma, ItalyView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 274–284https://doi.org/10.1145/115866.115895Online:01 May 1991Publication History 25citation375DownloadsMetricsTotal Citations25Total Downloads375Last 12 Months6Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

article Free Access Share on A note on Cohen's “eliminating redundant recursive calls” Author: Norman H. Cohen Softech Inc. 705 Masons Mill Business Park, Huntingdon Valley, PA 19006 Softech Inc. 705 Masons Mill Business Park, Huntingdon Valley, PA 19006View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 7Issue 4Oct. 1985 pp 680–685https://doi.org/10.1145/4472.215006Online:01 October 1985Publication History 0citation193DownloadsMetricsTotal Citations0Total Downloads193Last 12 Months4Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF