[marklemay]

ATS seems relevant, it has dependent types and linear types. My understanding isthat linear types have a lot in common with barrow checking.