Switch to: References

Add citations

You must login to add citations.
  1. Dependent choice as a termination principle.Thomas Powell - 2020 - Archive for Mathematical Logic 59 (3-4):503-516.
    We introduce a new formulation of the axiom of dependent choice, which can be viewed as an abstract termination principle that in particular generalises recursive path orderings, the latter being fundamental tools used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
    Download  
     
    Export citation  
     
    Bookmark  
  • Bar recursion over finite partial functions.Paulo Oliva & Thomas Powell - 2017 - Annals of Pure and Applied Logic 168 (5):887-921.
    Download  
     
    Export citation  
     
    Bookmark  
  • Bar recursion and products of selection functions.Martín Escardó & Paulo Oliva - 2015 - Journal of Symbolic Logic 80 (1):1-28.
    We show how two iterated products of selection functions can both be used in conjunction with systemTto interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over systemTto Spector’s bar recursion, whereas the other isT-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation