New Path Order for Exponential Time


In this talk I present the Exponential Path Order EPO*, a product of joint
work with Naohi Eguchi during my stay at JAIST. Inspired by a novel term
rewriting characterisation of the exponential time functions FEXP, this
order is carefully trimmed so that compatibility of TRSs implies
exponentially bounded runtime complexity. Moreover, the order is complete
in the sense that every exponential time function can be expressed by a TRS
compatible with an instance of EPO*.