型による制限を検証し、実施する処理は型検査と呼ばれ、コンパイル時（静的検査）と実行時（動的検査）のどちらかまたは両方のタイミングで行われる。型検査はコンパイラが行う意味解析の一部である。プログラミング言語が型の規則を強く適用するなら、つまり自動的な型変換を情報が失われないものに限定するなら、強く型付けされていると言い、そうでなければ弱く型付けされていると言う。
プログラミング言語で、型検査が実行時の式に関する同値性の検査なしに行われることがあるならば、その言語は静的型付けであるという。 静的型付けされた言語にはコンパイル時と実行時という型検査の2つの段階がある。これに加えてリンク時の段階を持つ処理系も存在する。プログラムのいくつかのモジュールが実行時に判明する他のモジュールの情報なしに個別に型検査されるのなら（分割コンパイル）、その言語にはコンパイル時の型検査が存在する。
プログラミング言語がメタデータに基づく実行時の（動的な）ディスパッチを持つならば、その言語は動的型付けであるという。 動的型付けでは実行パスによって変数が異なった型をもつので、型検査は実行時に行われることが多い。動的型を対象とした静的な型システムは通例、実行パスの概念を明示的に表現して、型がそれに依存することに対応しなければならない。
動的な型付けはスクリプト言語やRAD言語などによくみられる。インタプリタ言語では動的型が採用されることが多く、コンパイラ言語では静的型が採用されることが多い。
型検査がどのように働くのかを見るために、次の擬似コードを考える。var x;x := 5;x := "hi";
この例では、1行目でxという名の変数を宣言し、2行目でxに整数5を代入し、3行目でxに文字列"hi"を代入している。ほとんどの静的型付けの処理系ではこのようなコードは不正（型エラー）となる。なぜなら2行目と3行目でxに一貫性のない型の値を代入しているからである。
対照的に純粋な動的型付けの処理系では、型は変数ではなく値に付けられるので、上のようなコードが実行できる。動的型付け言語の処理系は間違った文や式を実行したときに、値の誤用に関するエラーを型エラーとして捕捉する。つまり、動的型付けはエラーをプログラムの実行中に捕捉する。動的型付けの典型的な実装ではプログラム中のすべての値が型情報を持ち、演算に値を使う前に型情報を確かめる。例を挙げる。var x := 5;var y := "hi";var z := x + y;
このコードでは、1行目でxに値5を束縛し、2行目でyに値"hi"を束縛し、3行目でxとyを足そうとしている。動的型付け言語ではxに束縛された値は(整数, 5)というペアとして表すことができ、yに束縛された値は(文字列, "hi")というペアで表すことができる。プログラムが3行目を実行しようとしたとき、処理系は整数と文字列という型情報を検査し、もし演算+（加算）がその2つの型について定義されていなかったら、エラーを出す。
プログラミング言語の中には、静的に型検査されないコードをプログラマが書けてしまう「バックドア」を持つものもある。例として、JavaやC風の言語には「キャスト」がある。
プログラミング言語が静的型付けをもつことは必ずしも動的型付けをもたないことを意味するわけではない。例えばJavaは静的型付けを採用しているが、処理によっては動的な型情報の取得を必要とするものもあり、それらは動的型付けの一形態とみなせる。静的型付けと動的型付けの違いについては様々な議論がある。
静的型付けか動的型付けかの選択はいくつかのトレードオフを必要とする。
静的型付けは型エラーをコンパイル時にある程度確実に発見する。よって最終的なプログラムの信頼性を上げるはずである。しかしながら、型エラーがどれほど犯しやすい間違いなのか、その内の何割が静的型付けで検出できるのか、という点についてプログラマの意見は割れている。静的型付けの支持者は型検査されたプログラムの方が信頼性が高いと信じており、それに対して動的型付けの支持者は実際に流通しているソフトウェアの信頼性では大差ない点を指摘している。 静的型付けの価値は型システムの強度が上がるにつれて高まっていくと考えられる。MLやHaskellなどの強く型付けされた言語の支持者は、プログラム中のデータ型を十分にプログラマが宣言するかコンパイラが推論すれかすれば、ほぼすべてのバグは型エラーとみなせると提案している。[2]
静的型付けは大抵、より高速に実行可能なコンパイル済みコードを生成する。コンパイラが正確なデータ型を知っていれば、最適化されたコードを生成できる。さらに、静的型付け言語のコンパイラではショートカットをみつけるのもより簡単になる。この理由からCommon Lispなどのいくつかの動的型付け言語では随意で型宣言ができるようになっている。最適化のための型付けは静的型付けの影響で普及した。
対照的に、動的型付けのほうがコンパイラやインタプリタの動作が高速になることがある。動的型付けの言語ではソースコードが変更されてもやり直すべき解析が少ないためである。これは「編集-コンパイル-テスト-デバッグ」というサイクルの時間を減らす。
型推論のない静的型付け言語（Javaなど）ではプログラマがメソッドや関数の型を宣言しなければならない。これはプログラムの追加的なドキュメントとして機能することがあり、コンパイラによってコードと同期させることが強制される。しかし型宣言のない静的型付け言語もあるので、これは静的型付けのというよりは型宣言の報酬である。
動的型付けはいくつかの静的型付けでは不正となり実現できない仕組みを可能にする。例えばデータをコードとして実行するeval関数である。さらに動的型付けでは、具体的なデータ構造の代わりに文字列を暫定的に用いることなどがやりやすく、プロトタイピングとの相性も良い。
動的型付け言語のメタプログラミング機能はより強力で使いやすいことが多い。例を挙げると、C++のテンプレートはRubyやPythonでの等価なコードより、書くのが煩わしい。またイントロスペクションのような、より高度な実行時の仕組みを静的型付け言語で使うのは、さらに困難になることが多い。
強い型付けの定義の1つは、ある処理・演算が間違った型の引数をとることを禁止するというものである。例えばCでは不正なキャストができるが、これは強い型付けが存在しないことを示している。コンパイルが通ってしまうというだけでなく、実行時にも許されてしまうからである。これはコンパクトで高速なCのコードを可能にするが、デバッグをさらに困難なものにする。
専門家の中には未定義の処理を引き起こさない言語を指して、メモリセーフ言語（あるいは単にセーフ言語）という用語を使う者もいる。そのような言語では配列の領域外にアクセスするようなことはない。
弱い型付けとは、言語が型の暗黙的な変換（またはキャスト）をするという意味である。再び例を挙げる。var x := 5;var y := "37";x + y;
弱い型付けの言語でこのようなコードを書くと、どのような（型の）結果が得られるのか自明ではない。Visual Basicなど、実行すると42という結果を出す言語もあり、そのような処理系は演算が意味のあるものになるように文字列"37"を数値の37に変換する。またJavaScriptなど、"537"という結果を出す言語もあり、そのような処理系は数値5を文字列"5"に変換し、文字列同士を連結する。どちらの言語でも、結果の型を決定する規則では両方のオペランド（演算子の左と右の値）が考慮されている。AppleScriptなどの言語では、結果の型は左のオペランドの型のみによって決定される。