DEMANGEON , Romain

We present a method for ensuring termination of lambda- calculi with references. This method makes it possible to combine measure- based techniques for termination of imperative languages with traditional approaches to termination in purely functional languages, such as logical relations. More precisely, the method lifts any termination proof...

We present a method for ensuring termination of lambda- calculi with references. This method makes it possible to combine measure-based techniques for termination of imperative languages with traditional approaches to termination in purely functional languages, such as logical relations. More precisely, the method lifts any termination proof...

An impure language is one that combines functional and imperative constructs. We propose a method for ensuring termination of impure concurrent languages that makes it possible to combine term rewriting measure-based techniques with traditional approaches for termination in functional languages such as logical relations. The method can be made...

International audience