Switch to: References

Add citations

You must login to add citations.
  1. η- conversions of IPC implemented in atomic F.Gilda Ferreira - 2017 - Logic Journal of the IGPL 25 (2):115-130.
    It is known that the β-conversions of the full intuitionistic propositional calculus translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering β-conversions can be derived. In the present article, we improve the previous result by analysing the translation of the η-conversions of the latter calculus into a technical variant of the former system. In fact, from the strong normalization of F∧at we (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • The computational content of atomic polymorphism.Gilda Ferreira & Vasco T. Vasconcelos - 2019 - Logic Journal of the IGPL 27 (5):625-638.
    We show that the number-theoretic functions definable in the atomic polymorphic system are exactly the extended polynomials. Two proofs of the above result are presented: one, reducing the functions’ definability problem in ${\mathbf{F}}_{\mathbf{at}}$ to definability in the simply typed lambda calculus and the other, directly adapting Helmut Schwichtenberg’s strategy for definability in $\lambda ^{\rightarrow }$ to the atomic polymorphic setting. The uniformity granted in the polymorphic system, when compared with the simply typed lambda calculus, is emphasized.
    Download  
     
    Export citation  
     
    Bookmark