Continuation (informatique)En informatique, la continuation d'un système est son futur, c'est-à-dire la suite des instructions qu'il lui reste à exécuter à un moment précis. C'est un point de vue pour décrire l'état de la machine. Dans certains langages de programmation, les continuations peuvent être manipulées explicitement en tant qu'objets du langage à part entière : on peut stocker la continuation courante dans une variable que l'on peut donc manipuler en tant que telle ; puis plus loin, on peut restaurer la continuation, ce qui a pour effet de dérouter l'exécution du programme actuel vers le futur que l'on avait enregistré.
Théorie des types homotopiquesvignette| Couverture de la Théorie des types homotopiques : Fondations univalentes des mathématiques. Dans la logique mathématique et de l’informatique, la théorie des types homotopiques (en anglais : Homotopy Type Theory HoTT) fait référence à différentes lignes de développement de la théorie des types intuitionnistes, basée sur l’interprétation des types comme des objets auxquels l’intuition de la théorie de l’homotopie s’applique.
New FoundationsEn logique mathématique, New Foundations (NF) est une théorie des ensembles axiomatique introduite par Willard Van Orman Quine en 1937, dans un article intitulé « New Foundations for Mathematical Logic », et qui a connu un certain nombre de variantes. Pour éviter le paradoxe de Russell, le principe de compréhension est restreint aux formules stratifiées, une restriction inspirée de la théorie des types, mais où la notion de type est implicite.
Langue SOVUne langue SOV est, en typologie syntaxique, une langue dont les phrases suivent, généralement, un ordre sujet-objet-verbe. D'après l'étude de 402 langues par Russell S. Tomlin publiée en 1986, 45 % des langues dans le monde suivent le modèle de SOV, et 75 % des langues naturelles sont des langues SOV ou SVO (sujet-verbe-objet). Cet ordre est le plus fréquent et représente environ 45 % des langues. Parmi les langues naturelles, SOV est le type le plus commun.
Méthode des tableauxvignette|200px|Représentation graphique d'un tableau propositionnel partiellement construit En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000).
