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

<p>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.</p>

CC BY-SA 4.0
2020-01-15T09:59:09.690Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-01-15T12:19:37.090Z
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?
Apoorv
CC BY-SA 4.0
2020-01-15T17:36:09.917Z
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?
Max New
CC BY-SA 4.0
2020-01-15T17:43:16.030Z
ah, indeed. I now understand why is it strange. I will fix it. Thank you!
Apoorv
<reference-request><pl.programming-languages><type-theory>
Equational Theories for Type Systems
Apoorv
# Equational Theories for Type Systems

(Asked by: username_0 on 2020-01-15)

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.

**Tags:** reference-request, pl.programming-languages, type-theory
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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?  
> **username_2**: 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?  
> **username_0**: ah, indeed. I now understand why is it strange. I will fix it. Thank you!  

---

## 0 answers

