[Checkers] Thoughts on Type Inference: Part 2 (inference for IGJ and in general)

[Michael Ernst]

Mahmood-

The general approach you endorse seems right to me.

These different descriptions boil down to the same thing, I think:

 * find the "inverse" of each operation
 * for each operation, determine what must be true about the input program
   in order for that operation to typecheck
 * determine the constraints that the operation places on the program

The latter is the more usual technical jargon.

> 1. Analysis to infer mutability, which is identical to Javari.

There is a core Javari algorithm.  Also, there are  various tweaks that add
additional type-variables (but don't change the algorithm), along with ways to
translate the inference results for those type-variables into Javari types
for program variables.  How much of the Javari analysis are you referring
to here?

                    -Mike