[gugagore]

We're not using "type theory" the same way, I think. I'm thinking in terms of

    - simply typed lambda calculus
    - System F
    - dependent type theory (MLTT)
    - linear types
    - row types
    - and so on

But it's subtle to talk about. It's not like there is a single type theory that underlies Typescript or Rust, either. These practical languages have partial, (and somewhat post-hoc) formalizations of their systems.

[pjmlp]

For starters,

"On the use of LISP in implementing denotational semantics"

https://dl.acm.org/doi/10.1145/319838.319866

Type theory in CS isn't a synonymous with whatever Haskell happens to do.