Section: New Results

λΠ-calculus modulo theory

G. Dowek has given a semantic criterion for the termination of the λΠ-calculus modulo theory. This result has been published in [23].

A. Assaf, G. Dowek, J.-P. Jouannaud and J. Liu have given a confluence criterion for untyped higher-order rewrite systems, and demonstrated some applications to the λΠ-calculus modulo theory.

G. Dowek has given an invited talk at PxTP where he has presented a state of the art of the production of system-independent proof libraries. This paper has been published in the proceedings of PxTP [12].