Summary: We give a characterisation of Bishop locally compact metric spaces in terms of formal topology. To this end, we introduce the notion of inhabited enumerably locally compact regular formal topology, and show that the category of Bishop locally compact metric spaces is equivalent to the full subcategory of formal topologies consisting of those objects which are isomorphic to some inhabited enumerably locally compact regular formal topology. In the course of obtaining the above equivalence, we show a couple of point-free results which are of independent interest. First, we show that any overt enumerably locally compact regular formal topology admits a one-point compactification, i.e. it can be embedded into a compact overt enumerably completely regular formal topology as the open complement of a formal point. Second, we characterise the class of enumerably completely regular formal topologies as the subtopolgies of the product of countably many copies of the formal unit interval. We work in Aczel's constructive set theory CZF with Regular Extension Axiom and Dependent Choice.