Is there a simple algorithm for proof search on CoC?

Question

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/elegant algorithm capable of solving this problem for a large class of terms? For example, given the term below:

λ (N : Type)
λ (S : {x : N} N)
λ (Z : N)
λ (A : {x : N} Type)
λ (B : {x : N} (A x))
λ (C : {x : (A (S (S (S Z))))} Type)
(C _)

The algorithm would replace _ by (B (S (S (S Z)))), as it is the only substitution that makes the resulting term well-typed. I'm specifically looking for keywords / references, as I believe this is a pretty well-researched subject (given that most theorem provers feature proof search), but I've never seen an algorithm described in a simpler setup (like plain CoC).

Answer 1

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.