Projet : Pour L'Utilisation et l'aMÉlioration
de la déduction automatique
Précédent : Modèles opérationnels des langages de
Remonter : Résultats nouveaux
Suivant : Autour de Coq
Un article [] reprend une étude antérieure sur la
normalisation forte (terminaison) de calculs substitutions explicites.
Il est montré que divers systèmes qui étaient conjecturés fortement
normalisables ne le sont en fait pas. Le résultat est intéressant par
lui-même, mais aussi il ouvre des perspectives pour la recherche de
calculs ayant de bonnes propriétés