Logique d'ordre supérieur
Les logiques d'ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d'utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats.
D'un point de vue sémantique, cela revient à dire que l'on considère les fonctions et prédicats comme des objets à part entière, au même titre que, par exemple, un nombre entier. On s'autorisera ainsi, d'une part, à quantifier les prédicats et fonctions et, d'autre part, à donner des fonctions ou des prédicats en arguments d'autres fonctions et prédicats. Néanmoins, on pourra se doter d'un système de typage qui restreindra le genre d'objet qui pourra être donné en tant que tel ou tel argument de tel ou tel prédicat ou telle ou telle fonction.
Les lambda-calculs typés s'inspirent de telles logiques dans ce qu'on appelle le paradigme fonctionnel. Un lien fort est tissé entre les mathématiques et l'informatique grâce à l'isomorphisme de Curry-Howard qui associe un lambda-calcul à une logique. C'est de ce domaine que sont issus les langages de programmation fonctionnelle.