# Termination of $\lambda$$\Pi$ modulo rewriting using the size-change principle (work in progress)

## TL;DR

This paper explores how the size-change termination principle can be applied to ensure termination in higher-order rewriting systems within dependent type theories, extending its original use in first-order functional programs.

## Contribution

It demonstrates the applicability of the size-change principle to higher-order rewriting in a dependent type setting, advancing termination analysis techniques.

## Key findings

- Size-change principle can be adapted for higher-order rewriting
- Extension of LF with termination guarantees
- Potential for improved termination proofs in dependent types

## Abstract

The Size-Change Termination 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.