Writing Programs That Construct Proofs, Constable et al. 1984.
Beautiful introduction. Quite readable without much knowledge. Discusses λ-PRL. Defines tactics and tacticals.
Constructive Mathematics and Automatic Program Writers, Constable 1971
Lots of literature here