13 September 2018

LSV library, 9:30-12:00

Programme:

• Adding injective symbols / conditional rewriting
• Remove brackets?
• Comparison of performances between Lambdapi and Dedukti (Rodolphe)
• Compatibility between Lambdapi and Dedukti (WHNF for example)
• Future syntax of Lambdapi (Rodolphe and Frédéric)
• Characters allowed in symbol names (Why /,+,*,%,=,@... are not allowed?) (Guillaume G.)
• Point on termination checker (G. Genestier)
• Point on Lambdapi user interface (Emilio?)
• Point on Lambdapi tactics (Aris and Franck)
• A new typing algorithm for rewrite rules to prove subject reduction