@article{HOFMANN2000113,
    Abstract = {In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni--Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK-algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and ⊸ as well as recursion over trees and other data structures remains within polynomial time. In its original formulation SLR supported only natural numbers and recursion on notation with first-order functional result type.},
    Author = {Hofmann, Martin},
    File = {1-s2.0-S0168007200000105-main (0) (0) - a - a - n.pdf},
    ISSN = {0168-0072},
    Journal = {Annals of Pure and Applied Logic},
    Keywords = {Type systems, Polynomial time, Realisability},
    Number = {1},
    Pages = {113 - 166},
    Title = {Safe recursion with higher types and BCK-algebra},
    URL = {http://www.sciencedirect.com/science/article/pii/S0168007200000105},
    Volume = {104},
    Year = {2000},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007200000105},
    bdsk-url-2 = {https://doi.org/10.1016/S0168-0072(00)00010-5},
    date-added = {2019-05-02 13:28:58 +0200},
    date-modified = {2019-05-02 13:28:58 +0200},
    doi = {10.1016/S0168-0072(00)00010-5}
}

@article{HOFMANN2000113, Abstract = {In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni--Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK-algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and ⊸ as well as recursion over trees and other data structures remains within polynomial time. In its original formulation SLR supported only natural numbers and recursion on notation with first-order functional result type.}, Author = {Hofmann, Martin}, File = {1-s2.0-S0168007200000105-main (0) (0) - a - a - n.pdf}, ISSN = {0168-0072}, Journal = {Annals of Pure and Applied Logic}, Keywords = {Type systems, Polynomial time, Realisability}, Number = {1}, Pages = {113 - 166}, Title = {Safe recursion with higher types and BCK-algebra}, URL = {http://www.sciencedirect.com/science/article/pii/S0168007200000105}, Volume = {104}, Year = {2000}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0168007200000105}, bdsk-url-2 = {https://doi.org/10.1016/S0168-0072(00)00010-5}, date-added = {2019-05-02 13:28:58 +0200}, date-modified = {2019-05-02 13:28:58 +0200}, doi = {10.1016/S0168-0072(00)00010-5} }