Semantic-Type-Guided Bug Finding

TL;DR

This paper introduces a new method for proving the incorrectness of semantic typing properties in functional programs, using a semantic type refuter that is both sound and complete.

Contribution

It extends incorrectness approaches to the model theory of functional program typing with a semantic type refuter that is co-recursively enumerable.

Findings

Refuter is co-recursively enumerable.

Refuter is sound and complete.

Implementation efficiently finds type errors.

Abstract

In recent years, there has been an increased interest in tools that establish \emph{incorrectness} rather than correctness of program properties. In this work we build on this approach by developing a novel methodology to prove incorrectness of \emph{semantic typing} properties of functional programs, extending the incorrectness approach to the model theory of functional program typing. We define a semantic type refuter which refutes semantic typings for a simple functional language. We prove our refuter is co-recursively enumerable, and that it is sound and complete with respect to a semantic typing notion. An initial implementation is described which uses symbolic evaluation to efficiently find type errors over a functional language with a rich type system.