Is there a simple algorithm for proof search on CoC?
Is there a simple algorithm? yes. Simply enumerate all possibilities.  Of course this is pretty intractable in practice.

A proper sub-problem of term generation in CoC is "higher-order unification".  It handles the simply typed lambda calculus.  It is undecidable.  But there is a classic practical solution by Huet.  There are a lot of resources here: https://stackoverflow.com/questions/1936432/higher-order-unification.

Now the only good reference I know for CoC term generation is "A Complete Proof Synthesis Method for the Cube of Type Systems" by Dowek.  I believe this summarizes his thesis work (in french) and there is a draft pdf floating around (it has some errors).  His r-splitting construction is a little awkward for implementations, but he does a good job of highlighting the difficulties, and suggesting practical in-complete solutions.