Théorie des langages de programmation

vignette|La lettre grecque minuscule λ (lambda) est un symbole non officiel de la théorie des langages de programmation. Cet usage dérive du lambda-calcul, un modèle de calcul introduit par Alonzo Church dans les années 1930 et largement utilisé par les chercheurs en langage de programmation. Il orne la couverture du texte classique Structure et interprétation des programmes informatiques, et apparaît dans le titre des fameux Lambda Papers de 1975 à 1980, écrits par Gerald Jay Sussman et Guy Steele, les développeurs du langage de programmation Scheme. La théorie des langages de programmation (Programming language theory ou PLT) est une branche de l'informatique qui traite de la conception, de la mise en œuvre, de l'analyse, de la caractérisation et de la classification des langages formels appelés langages de programmation. Elle est étroitement liée à d'autres domaines, notamment les mathématiques, le génie logiciel et la linguistique. Il existe un nombre important de conférences universitaires et de revues sur le sujet. Par certains aspects, l'histoire de la théorie des langages de programmation est antérieure au développement des langages de programmation eux-mêmes. Le lambda-calcul, développé par Alonzo Church et Stephen Cole Kleene dans les années 1930, est considéré par certains comme le premier langage de programmation au monde, même s'il était destiné à le calcul plutôt qu'à être un moyen pour les programmeurs de des algorithmes à un système informatique. Pourtant, de nombreux langages de programmation fonctionnels modernes sont désormais aisément décrits en termes de lambda-calcul. Le premier langage de programmation à être inventé fut Plankalkül, conçu par Konrad Zuse dans les années 1940, mais inconnu du public avant 1972 (et pas implémenté avant 1998). Le premier langage de programmation de haut niveau largement connu et populaire fut Fortran, développé entre 1954 et 1957 par une équipe de chercheurs d'IBM dirigée par John Backus.