Résumé
The indexing of syntactic terms is a key component for the efficient implementation of automated theorem provers. This paper presents the first verified implementation of a term indexing data structure, namely a formalization of path indexing in the proof assistant Isabelle/HOL. We define the data structure, maintenance operations, and retrieval operations, including retrieval of unifiable terms, instances, generalizations and variants. We prove that maintenance operations preserve the invariants of the structure, and that retrieval operations are sound and complete.