Skip to main content

All Questions

Filter by
Sorted by
Tagged with
7 votes
4 answers
1k views

What is the intuitive meaning of star and box in a pure type system?

The systems of the λ-cube have the axiom $\star:\square$. I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...
Matthew's user avatar
  • 303