New answers tagged

6

As you found out yourself, the answer to your question is yes. You found a rather convoluted example, a much simpler example is the following: $$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$ where $I$ and $K$ are the identity and first-projection combinators. This may be found at p. 204 of Sørensen and Urzyczyn's Lectures on the Curry-Howard Isomoprphism. They ...


4

So, after some research, I found that someone has formalized a proof of strong normalization of System F using the Calculus of Constructions + inductive types (see: A formalization of the strong normalization proof for System F in LEGO). This strongly suggests that one could write a System F interpreter in Coq. Erasing that interpreter to untyped lambda ...


0

Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your $\mathrm{reflexive}$ example, there are two polymorphic constants at play: $$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$ $$(=) : \...


Top 50 recent answers are included