System Fω
- Intrinsically kinded type operators for pure Fω
- Capture-avoiding binding laws for kinded type operators
- Semantic kind interpretation and substitution
- Proved type-beta conversion for pure Fω
- Type-beta confluence and conversion inversion
- Higher-kinded relational interpretation of Fω types
- Scoped pure Fω terms
- Erasure adapter to the existing System F scoped syntax
- Fω closing instances in the single existing term model
- Pure Fω typing with proved type-beta conversion
- Higher-kinded relational parametricity of pure Fω
- Conversion-aware weak call-by-value safety for pure Fω
- The star/forall System F fragment inside pure Fω
- System F embedding agreement with the single term/relation model
- Fω weak-CBV erasure into the existing full-beta term model
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.