John Halleck's site gives the axioms for Intuitionistic Propositional Logic using material implication, but lists those for Heyting's version thereof using strict implication where this page defines the notation. To make it more confusing, he cites Hackstaff 1966 which uses 'intuitionistic implication' (which is not clearly defined).
So, which implication should I use to properly encode Heyting's version of IPC? [The underlying exercise here is a formalization of many of the logics on Halleck's site, and so we want to stay true to the historical versions, even if it means we need to also have more versions so as to also encode more recent variants. Our techniques are such that the effort of adding variants is very low.]