Deaccumulation techniques for improving provability
From MaRDI portal
Publication:882487
DOI10.1016/j.jlap.2006.11.001zbMath1116.68077OpenAlexW2089817457MaRDI QIDQ882487
Armin Kühnemann, Jürgen Giesl, Janis Voigtländer
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
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins ⋮ Manipulating accumulative functions by swapping call-time and return-time computations ⋮ Polynomial-time inverse computation for accumulative functions with multiple data traversals
Uses Software
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
