<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>17</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Gilles Barthe</style></author><author><style face="normal" font="default" size="100%">Maria João Frade</style></author><author><style face="normal" font="default" size="100%">E. Giménez</style></author><author><style face="normal" font="default" size="100%">Luis Pinto</style></author><author><style face="normal" font="default" size="100%">Tarmo Uustalu</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Type-based termination of recursive definitions</style></title><secondary-title><style face="normal" font="default" size="100%">Mathematical Structures in Computer Science</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2004</style></year></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/mjf/files/tbterm.pdf</style></url></related-urls></urls><number><style face="normal" font="default" size="100%">1</style></number><volume><style face="normal" font="default" size="100%">14</style></volume><pages><style face="normal" font="default" size="100%">97-141</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;This paper introduces &quot;lambda-hat&quot;, a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system &quot;lambda-G&quot; in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to also support coinductive types and corecursive function definitions.&lt;/p&gt;
</style></abstract></record></records></xml>