Comment by nixpulvis
10 hours ago
I read the first post and thought someone should at the very least post the lambda cube. This isn't my area of expertise, since I've done very little with dependent types (staying firmly on the left side of the cube), but it outlines some useful categories of type systems here.
I wrote a small post on that: https://azdavis.net/posts/lambda-cube/
Hope it’s helpful!
Cool that you worked on an implementation of the CoC.
I've been somewhat wanting to go back and revisit ATAPL and read chapter 2 on this subject: https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf
That is a good post. I've linked to it from mine!
Thanks! But I don’t think it quite worked?
1 reply →