<p>The standard text book would be Benjamin Pierce, "Types and Programming Languages".</p>

<p>Technically, soundness is a property of a type system. Sometimes we also say informally that a type would be (un)sound for a given term, in the sense that the underlyung type system would be (un)sound if it allowed assigning this type.</p>

<p>Nowadays, type soundness is typically proved syntactically, as the combination of two properties: Preservation (every computation step maintains types) and Progress (a well-typed non-terminated program can always take another step). Both of these properties are proved by standard induction proofs over the reduction relation and the typing relation of the language, respectively, with the help of some auxiliary lemmas. Pierce's book explains this in much detail.</p>

<p>There also is the stronger notion of <em>semantic</em> type soundness, that additionally ensures that, e.g. abstraction cannot be broken. But that generally is much more difficult to prove and subject of ongoing research.</p>

CC BY-SA 4.0
2018-12-31T10:38:50.840Z
Small aside: type preservation does in general not hold for behavioural types (e.g. session types), so instead you have two notions of computation, one on programs and one on types, and one then proves that they co-evolve in sync.
Martin Berger
CC BY-SA 4.0
2018-12-30T15:14:57.210Z
2018-12-30T15:14:57.210Z
Andreas Rossberg
<p>For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that a type is sound, or it does not mean anything?</p>

<p>Also, how to demonstrate the soundness of a type or a type system? What is a good research-level textbook/reference on the topic?</p>

CC BY-SA 4.0
2019-01-01T11:07:52.463Z
Thsi question is better suited for cs.stackexchange.com. It is not research-level.
Andrej Bauer
<reference-request><type-theory><type-systems><soundness>
Soundness of type (systems)
Vincent
# Soundness of type (systems)

(Asked by: username_0 on 2018-12-30)

For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that a type is sound, or it does not mean anything?

Also, how to demonstrate the soundness of a type or a type system? What is a good research-level textbook/reference on the topic?

**Tags:** reference-request, type-theory, type-systems, soundness
> **Comments:**
> **username_1**: Thsi question is better suited for cs.stackexchange.com. It is not research-level.  

---

## 1 answers

### Answer by username_2 on 2018-12-30. Score: 1

The standard text book would be Benjamin Pierce, "Types and Programming Languages".

Technically, soundness is a property of a type system. Sometimes we also say informally that a type would be (un)sound for a given term, in the sense that the underlyung type system would be (un)sound if it allowed assigning this type.

Nowadays, type soundness is typically proved syntactically, as the combination of two properties: Preservation (every computation step maintains types) and Progress (a well-typed non-terminated program can always take another step). Both of these properties are proved by standard induction proofs over the reduction relation and the typing relation of the language, respectively, with the help of some auxiliary lemmas. Pierce's book explains this in much detail.

There also is the stronger notion of *semantic* type soundness, that additionally ensures that, e.g. abstraction cannot be broken. But that generally is much more difficult to prove and subject of ongoing research.

> **Comments:**
> **username_3**: Small aside: type preservation does in general not hold for behavioural types (e.g. session types), so instead you have two notions of computation, one on programs and one on types, and one then proves that they co-evolve in sync.  

---

