Please expand.
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}
}