@article{BARTHE_2004,
    doi = {10.1017/s0960129503004122},
    url = {https://doi.org/10.1017%2Fs0960129503004122},
    year = {2004},
    month = {feb},
    publisher = {Cambridge University Press ({CUP})},
    volume = {14},
    number = {1},
    pages = {97--141},
    author = {G. BARTHE and M. J. FRADE and E. GIMNEZ and L. PINTO and T. UUSTALU},
    title = {Type-based termination of recursive definitions},
    journal = {Mathematical Structures in Computer Science}
}

@article{BARTHE_2004, doi = {10.1017/s0960129503004122}, url = {https://doi.org/10.1017%2Fs0960129503004122}, year = {2004}, month = {feb}, publisher = {Cambridge University Press ({CUP})}, volume = {14}, number = {1}, pages = {97--141}, author = {G. BARTHE and M. J. FRADE and E. GIMNEZ and L. PINTO and T. UUSTALU}, title = {Type-based termination of recursive definitions}, journal = {Mathematical Structures in Computer Science} }