In informatica, un sistema dei tipi è un framework sintattico per la classificazione di espressioni secondo i tipi che esse calcolano.[1] Un sistema dei tipi associa tipi a ogni valore computato. Esaminando il flusso di questi valori, un sistema dei tipi tenta di dimostrare che non avvengano errori di tipo. Il sistema stesso determina che cosa costituisce un errore di tipo, garantendo che le operazioni che si aspettano un certo tipo di valore non siano utilizzate con valori per i quali quell'operazione non ha senso.
La profondità dei vincoli sui tipi e la maniera con cui essi vengono valutati dal sistema influenzano la cosiddetta tipizzazione del linguaggio di programmazione. Nel caso di polimorfismo dei tipi, un linguaggio può associare alla stessa operazione un diverso algoritmo per ogni tipo utilizzabile. Sebbene i sistemi dei tipi concreti utilizzati nei linguaggi di programmazione nascano da problemi di natura pratica di architetture dei calcolatori, implementazione dei compilatori e progetto dei linguaggi, esiste una branca dell'informatica, detta teoria dei tipi, che studia i diversi sistemi dei tipi.