A. Dans-dedukti-l-', Égalité dans Dedukti Le code ci-dessous est la définition de l'égalité qu'on a proposée dans la section 5.1.2. On y démontre la symétrie et la transitivité de cette opération à l

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Dedukti : a logical framework based on the ??-calculus modulo theory

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 Platform, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00822856

H. William-alvin, The formulae-as-types notions of construction, Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pp.479-490, 1980.