Congruence Types

Abstract We introduce a type-theoretical framework in which canonical term rewriting systems can be represented faithfully both from the logical and the computational points of view. The framework is based on congruence types, a new syntax which combines inductive, algebraic and quotient types. Congruence types improve on existing work to combine type theories with algebraic rewriting by making explicit the fact that the term-rewriting systems under consideration are initial models of an equational theory. As a result, the interaction gustavo: thesisween the type theory and the algebraic types (rewriting systems) is much more powerful than in previous work. Congruence types can be used (i) to introduce initial models of canonical term-rewriting systems (ii) to obtain a suitable computational behavior of a definable operation (iii) to provide an elegant solution to the problem of equational reasoning in type theory.

Authors

• Gilles Barthe
• Herman Geuvers

Keywords

No keywords are indexed for this paper.