Arctic Termination... Below Zero (2009)
Adam Koprowski, Johannes Waldmann
Abstract. We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with −∞,...
A Formalization of the Simply Typed Lambda Calculus in Coq (2009)
Abstract. In this paper we present a formalization of the simply typed lambda calculus with constants and with typing `a la Church. It has been accomplished using the theorem prover Coq. The...
Automated Verification of Termination Certificates (2009)
Blanqui, Frédéric, Koprowski, Adam
Termination is an important property required for total correctness of programs/algorithms. In particular it is a well studied subject in the area of term rewriting, where a number of methods and...
Automated Verification of Termination Certificates (2009)
Blanqui, Frédéric, Koprowski, Adam
Termination is an important property required for total correctness of programs/algorithms. In particular it is a well studied subject in the area of term rewriting, where a number of methods and...
Techniques and theory used in TPA (2008)
Abstract. This document describes all the theorems used by proofs generated by TPA ver. 1.1, that took part in the Termination Competition 2006 [1]. Theorems in this document are identified by short...
A Formalization of the Simply Typed Lambda Calculus in Coq (2008)
Abstract. In this paper we present a formalization of the simply typed lambda calculus with constants and with typing à la Church. It has been accomplished using the theorem prover Coq. The...
Predictive labeling with dependency pairs using SAT (2008)
Adam Koprowski, Aart Middeldorp
Abstract. This paper combines predictive labeling with dependency pairs and reports on its implementation. Our starting point is the method of proving termination of rewrite systems using semantic...
1 CoLoR: a Coq Library on Rewriting and termination (2008)
Solange Coupet-grimal, William Delobel, Adam Koprowski
Abstract. Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs. 1.1 Introduction Termination is an important and difficult problem. Many...
Application of Rewriting Techniques to Verification Problems (2008)
Abstract. The goal of the project is to employ techniques from term rewriting to verification problems. The relationship between liveness properties and termination of term rewrite systems (TRSs) is...
Predictive labeling with dependency pairs using SAT (2008)
Adam Koprowski, Aart Middeldorp
Abstract. This paper combines predictive labeling with dependency pairs and reports on its implementation. Our starting point is the method of proving termination of rewrite systems using semantic...
A Formalization of the Simply Typed Lambda Calculus in Coq (2008)
Abstract. In this paper we present a formalization of the simply typed lambda calculus with constants and with typing à la Church. It has been accomplished using the theorem prover Coq. The...
Application of Rewriting Techniques to Verification Problems (2008)
The goal of the project is to employ techniques from term rewriting to verification problems. The relationship between liveness properties and termination of term rewrite systems (TRSs) is of...
A Formalization of the Simply Typed Lambda (2008)
Calculus In Coq, Adam Koprowski
In this paper we present a formalization of the simply typed lambda calculus with constants and with typing a la Church. It has been accomplished using the theorem prover Coq. The formalization...
Recursive Path Ordering for Infinite Labelled (2008)
Rewrite Systems Adam, Adam Koprowski, Hans Zantema
Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for automatic...
Certification of proving termination of term rewriting by matrix interpretations (2007)
We develop a Coq formalization of the matrix interpretation method, which is a recently developed, powerful approach to proving termination of term rewriting. Our formalization is a contribution to...
Certification of proving termination of term rewriting by matrix interpretations (2007)
Abstract. We develop a Coq formalization of the matrix interpretation method, which is a recently developed, powerful approach to proving termination of term rewriting. Our formalization is a...
Certification of matrix interpretations in Coq (2007)
Abstract. We describe how to certify the matrix interpretation method for proving termination of term rewriting in the theorem prover Coq. Certification requires both the formalization of the...
CoLoR: a Coq library on rewriting and termination (2006)
Blanqui, Frédéric, Coupet-Grimal, Solange, Delobel, William, Hinderer, Sébastien, Koprowski, Adam
Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
CoLoR: a Coq library on rewriting and termination (2006)
Blanqui, Frédéric, Coupet-Grimal, Solange, Delobel, William, Hinderer, Sébastien, Koprowski, Adam
Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
CoLoR: a Coq library on rewriting and termination (2006)
Blanqui, Frédéric, Coupet-Grimal, Solange, Delobel, William, Hinderer, Sébastien, Koprowski, Adam
Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
CoLoR: a Coq library on rewriting and termination (2006)
Blanqui, Frédéric, Coupet-Grimal, Solange, Delobel, William, Hinderer, Sébastien, Koprowski, Adam
Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
CoLoR: a Coq library on rewriting and termination (2006)
Blanqui, Frédéric, Coupet-Grimal, Solange, Delobel, William, Hinderer, Sébastien, Koprowski, Adam
Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.
TPA: Termination proved automatically (2006)
TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the technique...
Certified higher-order recursive path ordering (2006)
Abstract. Recursive path ordering (RPO) is a well-known reduction ordering introduced by Dershowitz [6], that is useful for proving termination of term rewriting systems (TRSs). Jouannaud and Rubio...
TPA: Termination Proved Automatically (2006)
Adam Koprowski Technical, Adam Koprowski
TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the technique...
Certified Higher-Order Recursive Path Ordering Adam Koprowski (2006)
Recursive path ordering (RPO) is a well-known reduction ordering introduced by Dershowitz [6], that is useful for proving termination of term rewriting systems (TRSs). Jouannaud and Rubio generalized...
Automation of recursive path ordering for infinite labelled rewrite systems (2006)
Abstract. Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for...
TPA: Termination proved automatically (2006)
Abstract. TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the...
Certified higher-order recursive path ordering (2006)
Abstract. The paper reports on a formalization of a proof of wellfoundedness of the higher-order recursive path ordering (HORPO) in the proof checker Coq. The development is axiom-free and fully...
1 CoLoR: a Coq Library on Rewriting and termination (2006)
Frédéric Blanqui, Solange Coupet-grimal, William Delobel, Adam Koprowski
Abstract. Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs. Termination is an important and difficult problem. Many criteria have been...
Automation of recursive path ordering for infinite labelled rewrite systems (2006)
Abstract. Semantic labelling is a transformational technique for proving termination of Term Rewriting Systems (TRSs). Only its variant with finite sets of labels was used so far in tools for...
Proving Liveness with Fairness using Rewriting (2005)
In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (TRSs) can be applied to prove...
Proving Liveness with Fairness using Rewriting (2005)
We show how the problem of verifying liveness properties in fair computations is related to relative termination of term rewrite systems (TRSs), extending [3]. We present a new transformation that is...
Proving liveness with fairness using rewriting (2005)
Abstract. We show how the problem of verifying liveness properties in fair computations is related to relative termination of term rewrite systems (TRSs), extending [3]. We present a new...
Proving liveness with fairness using rewriting (2005)
Abstract. In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (TRSs) can be applied...
Proving liveness with fairness using rewriting (2005)
Abstract. We show how the problem of verifying liveness properties in fair computations is related to relative termination of term rewrite systems (TRSs), extending [3]. We present a new...
Proving liveness with fairness using rewriting (2005)
Abstract. We show how the problem of verifying liveness properties in fair computations is related to relative termination of term rewrite systems (TRSs), extending [2]. We present a new...
Well-foundedness of the recursive path ordering in Coq (2004)
Nicole De Kleijn, Adam Koprowski, Femke Van Raamsdonk
The recursive path ordering due to Dershowitz is one of the important methods to prove termination of first-order term rewriting. The generalization to the higher-order case is due to Jouannaud and...