I was reading through Gunter's Semantics of Programming Languages: Structure and Techniques and in the second chapter on simply typed $\lambda$ calculus he introduces an equational theory with $\beta\eta\xi$ equality $T \vdash (H \triangleright M = N : \tau)$

What are the references for different equational theories for standard type systems such as Hindley-Milner, System F, substructural logics such as linear logic, etc.

  • 3
    $\begingroup$ This is a strange question. You quote one particular theorem, and then you ask a general reference question. Can you be a bit more precise what you're looking for? Also, I don't think there is a single book that has al the things you listed. $\endgroup$ Jan 15, 2020 at 9:59
  • $\begingroup$ I am not looking for one reference, a list of references is also okay. I expect equational theory for linear type system to have different set of equations but to have a similar theorem as one for STLC given in a Gunter. I will edit the question to make this clear. Does the question make more sense now? $\endgroup$
    – Apoorv
    Jan 15, 2020 at 12:19
  • 2
    $\begingroup$ I agree with Andrej that your question is a bit strange to an expert. Based on the last paragraph it looks like you are interested in a bunch of references for equational theories of calculi. The theorem you cite on the other hand is not an "interesting" theorem about equational theories, it is more like "basic hygiene", similar to saying that if $H \vdash M : \tau$ holds then $\tau$ is a well-formed type under $H$. Maybe just delete the statement of the theorem and the question would make more sense? $\endgroup$
    – Max New
    Jan 15, 2020 at 17:36
  • $\begingroup$ ah, indeed. I now understand why is it strange. I will fix it. Thank you! $\endgroup$
    – Apoorv
    Jan 15, 2020 at 17:43


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.