Le l-calcul est un formalisme introduit par Church dans les années trente: alors que dans le formalisme de Zermelo-Frankel les objets primitifs sont les ensembles, dans celui de Church, les objets primitifs sont les fonctions; et la notion de calcul (évaluation, réduction, réécriture) se trouve propulsée au premier plan.

L'intérêt pour le l-calcul s'est considérablement renouvelé avec la prolifération des ordinateurs et des langages informatiques. C'est que la plupart de ces langages comportent une partie "fonctionnelle" qui se comprend naturellement comme une implémentation du l-calcul. Le l-calcul constitue ainsi une plate-forme privilégiée pour la description et l'étude des langages informatiques, et à ce titre, il fait l'objet de développements intensifs.

On essayera, à travers des exemples, de donner une idée sur la richesse des formules du l-calcul, et sur les manipulations (réductions) qu'on leur fait subir. Puis on mentionnera les théorèmes principaux de la théorie de base (confluence, normalisation forte, sûreté). S'il reste du temps, on fera allusion au principe de Curry-Howard ((preuve: proposition) = (terme: type)) et/ou au polymorphisme. L'exposé n'exigera aucune connaissance préalable de l'auditoire.