Apparently, Chrząszcz implemented ML-style modules in Coq around 2003, and wrote a couple of papers and a PhD thesis. Which seems not available online (https://www.theses.fr/2004PA112014); only the abstract is (https://www.mimuw.edu.pl/sites/default/files/chrzaszcz_autoreferat.pdf). I wonder if that would be worth fixing, even if undoubtedly it'll take some waiting.
I stand corrected: it's at https://www.mimuw.edu.pl/~chrzaszcz/papers/thesis/ (linked from https://www.mimuw.edu.pl/~chrzaszc/papers/). I was misled because Scholar didn't seem to find it.
Last updated: Jan 29 2023 at 03:28 UTC