Deaccumulation techniques for improving provability
type: Item
instance of: scholarly article
title: Deaccumulation techniques for improving provability
zbMATH Open document ID: 1116.68077
author: Jürgen Giesl
author: Armin Kühnemann
author: Janis Voigtländer
published in: The Journal of Logic and Algebraic Programming
publication date: 2007-05-23T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5156681
zbMATH Keywords: tree transducers
zbMATH Keywords: induction theorem proving
zbMATH Keywords: tail recursion
zbMATH Keywords: program transformation
zbMATH Keywords: program verification
describes a project that uses: AProVE
describes a project that uses: RRL
MaRDI profile type: Publication
full work available at URL: j.jlap.2006.11.001
OpenAlex ID: W2089817457
cites work: Mechanizing structural induction. II: Strategies
cites work: Q3947094
cites work: The promotion and accumulation strategies in transformational programming
cites work: Implicit induction in conditional theories
cites work: The automation of proof by mathematical induction
cites work: Rippling: A heuristic for guiding inductive proofs
cites work: A Transformation System for Developing Recursive Programs
cites work: Computer Aided Verification
cites work: Invariance and non-determinacy
cites work: Bottom-up and top-down tree transformations— a comparison
cites work: A comparison of pebble tree transducers with macro tree transducers
cites work: Macro tree transducers
cites work: Modular tree transducers
cites work: How to design programs. An introduction to programming and computing
cites work: Q3925893
cites work: Q4210160
cites work: Q2723934
cites work: Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
cites work: An axiomatic basis for computer programming
cites work: Automatic verification of functions with accumulating parameters
cites work: Q2766775
cites work: Q3149665
cites work: The Substitution Vanishes
cites work: Programming Languages and Systems
cites work: FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
cites work: Recursive functions of symbolic expressions and their computation by machine, Part I
cites work: Swapping Arguments and Results of Recursive Functions
cites work: Q3996676
cites work: Q4414308
cites work: Theoretical Aspects of Computing - ICTAC 2004
cites work: Mappings and grammars on trees
cites work: Shortcut fusion for accumulating parameters & zip-like functions
cites work: Generalized sequential machine maps
cites work: Functional description of the contextual analysis in block-structured programming languages: A case study of tree transducers
cites work: Concatenate, reverse and map vanish for free
cites work: Using circular programs to deforest in accumulating parameters
cites work: Composition of functions with accumulating parameters
cites work: Q4296747
DOI: 10.1016/J.JLAP.2006.11.001
description: scientific article; zbMATH DE number 5156681