System F
- The existing untyped beta-conversion term model
- Binary beta-invariant relations
- Scoped pure System F
- System F erasure and closing environments
- Impredicative binary interpretation of System F types
- Type-substitution algebra for impredicative System F
- The five typing rules of pure System F
- Relational parametricity for pure System F
- Call-by-value safety for pure System F
- The call-by-value erasure bridge
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.