Thursday 25 July 2019, 10:30, LSV library: Subject reduction in Lambdapi and injectivity of function symbols, 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. The subject reduction is known to be equivalent to the well-typedness of rewrite rules if the rewrite system considered is confluent. We propose an algorithm for checking the well-typedness of rewrite rules. The use of unification modulo rewriting procedure in this algorithm gives rise to the idea of having an injectivity-checking function 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.