Switch to: References

Add citations

You must login to add citations.
  1. A solution to Curry and Hindley’s problem on combinatory strong reduction.Pierluigi Minari - 2009 - Archive for Mathematical Logic 48 (2):159-184.
    It has often been remarked that the metatheory of strong reduction $\succ$ , the combinatory analogue of βη-reduction ${\twoheadrightarrow_{\beta\eta}}$ in λ-calculus, is rather complicated. In particular, although the confluence of $\succ$ is an easy consequence of ${\twoheadrightarrow_{\beta\eta}}$ being confluent, no direct proof of this fact is known. Curry and Hindley’s problem, dating back to 1958, asks for a self-contained proof of the confluence of $\succ$ , one which makes no detour through λ-calculus. We answer positively to this question, by extending (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Analytic proof systems for λ-calculus: the elimination of transitivity, and why it matters. [REVIEW]Pierluigi Minari - 2007 - Archive for Mathematical Logic 46 (5-6):385-424.
    We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free derivations—of a number (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation