Dependent Types From Counterexamples

Motivated by recent research in abstract model checking, the authors present a new approach to inferring dependent types. Unlike many of the existing approaches, their approach does not rely on programmers to supply the candidate (or the correct) types for the recursive functions and instead does counterexample-guided refinement to automatically generate the set of candidate dependent types. The main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found un-typable with the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real type error or generate additional candidate dependent types to refute the spurious counterexample.