Ça c’est pile dans mes cordes. Utiliser un calculus bien défini, le modifier et prouver des propriétés … miam miam ;-)
C'est bien à peu près ça.
Idéalement il faudrait aussi quelques analyses de performance, soit avec de vrai benchmarks, soit avec des arguments "analytiques/symboliques".
Je suis motivé pour participer.
Tu peux commencer par lire "A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi", http://www-users.cs.umn.edu/~gopalan/papers/suspension-calculus.pdf
Cet article couvre les 2 "concurrents" principaux (le système principal présenté et le λσ). Il y manque par contre une version limitée antérieure du "Suspension Calculus", mais si non ça couvre assez bien le sujet.
Stefan