XML is becoming the de facto standard for information exchange. XML querying is a key component for structured information processing and plays a central role in the next generation world wide web, information management systems and databases. Applications relying on XML processing notably depend on XPath, the standard language for adressing parts of XML documents. Besides its fundamental functionality, reasons behind XPath suc- cess include being widely accepted by programmers and well-suited for formal treatments. With the growing volume of XML content and XML processing applications, our research is oriented toward efficiency of XML querying. Our approach relies on analysis and trans- formation of XPath expressions for optimization. This note presents current open issues with XPath, and introduces our preliminary results applied to streaming XPath processing. Moreover, it describes our methodology, which includes XPath modelisation using the Coq proof assistant, and future directions envisioned toward high performance XML querying.