Deaccumulation techniques for improving provability

DOI10.1016/j.jlap.2006.11.001zbMath1116.68077MaRDI QIDQ882487

Jürgen Giesl, Janis Voigtländer, Armin Kühnemann

Publication date: 23 May 2007

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2006.11.001

zbMATH Keywords

program transformation; program verification; tree transducers; tail recursion; induction theorem proving

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q60: Specification and verification (program logics, model checking, etc.)

Uses Software

• AProVE
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Modular tree transducers
• Macro tree transducers
• Mechanizing structural induction. II: Strategies
• Functional description of the contextual analysis in block-structured programming languages: A case study of tree transducers
• A comparison of pebble tree transducers with macro tree transducers
• Using circular programs to deforest in accumulating parameters
• Implicit induction in conditional theories
• Generalized sequential machine maps
• Concatenate, reverse and map vanish for free
• Shortcut fusion for accumulating parameters & zip-like functions
• Recursive functions of symbolic expressions and their computation by machine, Part I
• The promotion and accumulation strategies in transformational programming
• Invariance and non-determinacy
• Swapping Arguments and Results of Recursive Functions
• The Substitution Vanishes
• Bottom-up and top-down tree transformations— a comparison
• A Transformation System for Developing Recursive Programs
• Automatic verification of functions with accumulating parameters
• Composition of functions with accumulating parameters
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Mappings and grammars on trees
• Theoretical Aspects of Computing - ICTAC 2004
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Computer Aided Verification