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?

  • $\begingroup$ Thsi question is better suited for cs.stackexchange.com. It is not research-level. $\endgroup$ – Andrej Bauer Jan 1 '19 at 11:07

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.

  • $\begingroup$ 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. $\endgroup$ – Martin Berger Dec 31 '18 at 10:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.