Termination of Lambda-Pi modulo rewriting using the size-change principle
Authors: Guillaume Genestier and Frédéric Blanqui
Paper Information
| Title: | Termination of Lambda-Pi modulo rewriting using the size-change principle |
| Authors: | Guillaume Genestier and Frédéric Blanqui |
| Proceedings: | WST WST2018proceedings |
| Editor: | Salvador Lucas |
| Keywords: | Dependant Types, Higher-Order Rewriting, Termination, Lambda-calculus |
| Abstract: | ABSTRACT. The Size-Change Principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types extending LF. |
| Pages: | 1 |
| Talk: | Jul 19 16:00 (Session 136H: Higher-Order) |
| Paper: | ![]() |
