* However I wonder what's left after you remove the issues I mentioned above. There are two cases: typed language and untyped language. In the first case you're

* However I wonder what's left after you remove the issues I mentioned above. There are two cases: typed language and untyped language. In the first case you're left with Type Theory. In the second case you're left with, either a Turing Machine or a Lambda Calculus (e.g., implemented in a syntax free language like scheme). Is this the correct line of thinking? Or is there more to PLT than what I described?* Well, there's still what you describe in the rest of your post. Even something minimalist like Scheme has a load of features above and beyond plain lambda calculus: dynamic parameters, continuations, dynamic-wind, mutable variables, boxes, exceptions, the whole macro system, and so on. Not every programming language feature that can exist has already been invented. We also don't fully understand the implications of every language feature that has already been invented -- there's plenty of work to do in designing type systems that can cope with more language features. You're not going to find one book that covers every feature people have come up with, but PLAI at least gives a fairly broad guided tour. I would add a book on semantics (probably Winskel, maybe Gunter) to develop a mental toolkit for carefully defining and reasoning about new language features.