Sur la sémantique des effets calculatoires

L'étude de la sémantique des langages de programmation est liée à un grand nombre de domaines, parmi lesquels la théorie de la démonstration en logique. Ces connexions ont permis des avancées communes dans les deux domaines : on comprend aujourd'hui comment l'étude des effets calculatoires en sémantique se traduit dans les systèmes logiques, comme par exemple le calcul dual de Curien et Herbelin. Dans cet exposé, je présente ces domaines selon une perspective historique, et j'esquisse le début d'un travail sur l'enrichissement de ce calcul pour tenir compte de davantage d'effets.