プログラミング言語の型システムを分類する3つめの方式は、型付けされた処理や型変換の安全性によるものである。計算機科学ではある言語が誤った状態を引き起こす処理や変換を許さないとき、その言語は「型安全（type-safe）」であるという。
例を再掲する。var x := 5;var y := "37";var z := x + y;
前述したように、Visual Basicなどの言語では変数zの値は42となる。この動作がプログラマの意図したものであってもそうでなくとも、言語はこの結果を明確に定義しており、プログラムがクラッシュしたり、zに不定な値が代入されてしまうようなことはない。このような動作をする言語は型安全である。
Cで同じ例を考えてみる。int x = 5;char y[] = "37";char* z = x + y;
この例ではzはyのアドレスに5バイト加えた先のメモリの内容を参照する。言い換えればyが指す文字列の終端のヌル文字の2バイト先を指している。その位置のデータは不定（プログラムで定義されていない）であり、おそらくアドレス可能なメモリの外側にあるので、ここでzをデリファレンスするとプログラムの終了を引き起こすことがある。これは型付けされているが、メモリセーフではないプログラムの例である。型安全な言語ではこのような状況は起こりえない。
詳細はポリモーフィズムを参照
ポリモーフィズムという単語は、コード（具体的には関数やクラス）が複数の型の値に基づいて動作できること、または同じデータ構造の異なるインスタンスが異なった型の要素を持てることを指す。型システムによってはコードの再利用性を改善するためにポリモーフィズムを持つものもある。ポリモーフィズムのある言語ではプログラマはリストや連想配列のようなデータ構造を使用される要素の型ごとにではなく、単に一度だけ実装すればよい。この理由から計算機科学ではこの種のポリモーフィズムの利用はジェネリックプログラミングと呼ばれることがある。ポリモーフィズムの型理論における基礎は抽象化やモジュール、また（場合によっては）派生型についての研究と密接な関連がある。
プログラミング環境によっては、2つのオブジェクトの間に全く関係がなくともそれらが同じ型を持つことがある。例としてはC++のポインタとiteratorの双対性が挙げられる。両方とも * 演算が定義されているが、全く別のメカニズムによって実装されている。
このテクニックは「ダック・タイピング（Duck Typing）」と呼ばれる。由来は次の警句である。"If it waddles like a duck, and quacks like a duck, it's a duck!"
詳細は型推論を参照
多くの静的な型システム（例えば C や Java）は型宣言を必要とし、プログラマはすべての変数に特定の型を明示的に関連付けなければならない。そうでないもの（例えば Haskell）は型推論を行い、コンパイラはプログラマの変数に対する扱いから変数の型についての結論を引き出す。例として、x と y を足す関数 f(x, y) を仮定すると、コンパイラは加算は数値のみに定義されているので x と y は共に数値であると推論できる。ゆえにプログラム中で f の引数として数値でない型（文字列やリストなど）を取って呼び出すとエラーを報告する。
コード中の数値や文字列のリテラルおよび式は型を暗示する。例えば、式 3.14 はおそらく浮動小数点数を暗示し、式 1, 2, 3 はおそらく整数のリスト（主に配列）を暗示する。
静的型付け言語の型検査では、すべての式の型がその式が現れた文脈で期待される型と一貫しているか、検証しなければならない。たとえば、x := eという代入文では式eの推論される型は変数xの宣言型または推論型と一貫していなければならない。この一貫性の概念を互換性といい、プログラミング言語ごとに固有のものである。
明らかなように、eとxの型が同一でかつその型への代入操作が許可されているなら、これは正当な式である。したがって最も単純な型システムでは、2つの型が互換であるかどうかは2つの型が同一である（または等価である）かどうか（等価性）という単純な問題に置き換えることができる。別の言語では2つの式が同じ型を持つと理解されるのに別の基準を採用している。これら、型の同一性理論は非常に多岐にわたっており、2つの極端な例は structural typing と nominative typing である。structural typing とは同じ外部構造（インタフェース、特に暗黙的なもの）を持つ値を同じ型であるとするもので、nominative typing とは型宣言の構文からのみ型の同一性を判定する（型が同じ「名前」を持たなければならない）ものである。
派生型のある言語では互換性の関係はより複雑なものとなる。型Aが型Bの派生型であるとすると、A型の値はB型の値が必要とされる文脈で使用することができる。しかし逆は真ではない。等価性と同様に派生型の関係はプログラミング言語によって異なった方法で定義され、多くのバリエーションが存在しうる。パラメータ付けされたまたはアドホックなポリモーフィズムを持つ言語の存在は型の互換性に何らかの意味を持つのかもしれない。
静的および強い型付けの支持者と動的および自由な型付けの支持者の間では衝突が度々おきる。前者のグループは厳密な型付けの使用によって、処理系がより多くのエラーを問題が大きくなる前に発見できるようになると主張している。後者のグループはより気軽な型付けによってコードはよりシンプルなものになり、そのようなコードは解析しやすいとされるので、エラーは減少すると主張している。型推論がある言語では型を手で宣言する必要はほとんどないので、強い型付けに伴う開発のオーバーヘッドは低減される。
個人がどのグループに分かれるかは、開発しているソフトウェアの種類やチームのメンバーの能力、他のシステムとの対話性の度合い、開発チームの規模などに依ることが多い。少人数で小回りのきくプロジェクトには気軽な型付けがより合い、フォーマルで大人数で仕事が分断されている（プログラマ、アナリスト、テスト部隊、など）プロジェクトは厳密な型付けのほうがうまくいくことが多い、と結論づける者もいる。
[ヘルプ]
^ 抽象データ型や関数型などのように実行時に値の集合として表現できない型もある
^ ⇒http://citeseer.ist.psu.edu/xi98dependent.html
参考資料
⇒Advanced Topics in Types and Programming Languages by Benjamin C. Pierce
⇒Type System Terminology
Meijer, Erik and Peter Drayton. " ⇒Static Typing Where Possible, Dynamic Typing When Needed: The End of the Cold War Between Programming Languages". Microsoft Corporation. 2007-03-08 閲覧。