Cynthia Kop ; Femke van Raamsdonk - Dynamic Dependency Pairs for Algebraic Functional Systems

lmcs:668 - Logical Methods in Computer Science, June 19, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:10)2012
Dynamic Dependency Pairs for Algebraic Functional SystemsArticle

Authors: Cynthia Kop ; Femke van Raamsdonk

    We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate {\beta}-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.

    https://doi.org/10.2168/LMCS-8(2:10)2012
    Source: arXiv.org:1205.2519
    Volume: Volume 8, Issue 2
    Published on: June 19, 2012
    Imported on: November 11, 2011
    Keywords: Computer Science - Logic in Computer Science,F4.1,F4.2
    Licence: arXiv.org - Non-exclusive license to distribute
    Funding:
      Source : OpenAIRE Graph
    • Higher-Order Termination; Funder: Netherlands Organisation for Scientific Research (NWO); Code: 612.000.629

    Publications

    IsCitedBy
    Size-Based Termination for Non-Positive Types in Simply Typed Lambda-Calculus
    • 1 ScholeXplorer

    References

    Share and export

    Consultation statistics

    This page has been seen 806 times.
    This article's PDF has been downloaded 274 times.