| Towards Formalizing Parametricity For Nested Types In Agda |
2021 |
721 |
Recent work by Johann, Ghiorzi, and Jeffries presents a Hindley-Milner-style calculus whose type system includes a primitive type formation rule for constructing nested types directly as fixpoints. The term calculus for this type system supports prim... |