Abstract: We present a general framework for termination proofs for Higher-Order Rewrite Systems. The method is tailor-made for having simple (and modular) proofs showing the termination of enriched lambda-calculi.
Previous | Index | Next An error occured whilst processing this directive