FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: