Wednesday 04 September 2019, 14:00, LSV library: Subject reduction in Lambdapi and injectivity of function symbols in term rewriting, Jui-Hsuan (M1 intern, ENS Ulm).

Lambdapi is a new proof assistant based on the lambda-pi calculus modulo that extends the lambda-pi calculus with user-defined rewrite rules. To guarantee good meta-properties of the proof system, the subject reduction property should be verified. In this talk, We propose an algorithm for checking the type preservation property of rewrite rules, which is equivalent to the subject reduction for rewrite rules. The use of unification modulo rewriting procedure in this algorithm gives rise to the idea of having of an injectivity-checking algorithm for retrieving more information from constraints. We propose an algorithm which gives a sufficient condition for injectivity. Finally, we will give some examples to show how these algorithms work.