Dependent ML

Please expand.

References

Dependent ML was first presented in a PLDI 1998 paper:

Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation (PLDI '98). Association for Computing Machinery, New York, NY, USA, 249–257. https://doi.org/10.1145/277650.277732

@inproceedings{10.1145/277650.277732,
	author = {Xi, Hongwei and Pfenning, Frank},
	title = {Eliminating Array Bound Checking through Dependent Types},
	year = {1998},
	isbn = {0897919874},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	url = {https://doi.org/10.1145/277650.277732},
	doi = {10.1145/277650.277732},
	booktitle = {Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation},
	pages = {249–257},
	numpages = {9},
	location = {Montreal, Quebec, Canada},
	series = {PLDI '98}
}