Dynamically typed languages enable programmers to write elegant, reusable and extendable programs. Recently, some progress has been made regarding their verification. However, the user is currently required to manually show the absence of type errors, a tedious task usually involving large amounts of repetitive work.

As most dynamically typed programs only occasionally divert from what would also be possible in statically typed languages, properly designed type inference algorithms should be able to supply the missing type information in most cases. We propose integrating a certified type inference algorithm into an interactive verification environment in order to a) provide a layer of abstraction, allowing the users to verify their programs like in a statically typed language whenever possible and b) use verification results to improve type inference and thus allow type checking of difficult cases.

Additionally, the common idiom of interacting with polymorphic data in such languages poses another challenge for verification. Some ideas for verifying such polymorphic methods in a type-independent way will also be discussed.

As this is work in progress, we will present our approach rather informally on the basis of small examples.