Structural Resolution meets Curry-Howard

Mathematical induction is pervasive in programming and program verification. It arises in data definitions (e.g., it describes some algebraic data structures), it underlies program semantics (e.g., it explains how to reason about finite iteration and recursion), and it gets used in proofs (e.g., it supports lemmas about data structures used in inductive proofs). Coinduction, too, is important in programming and program verification. It arises in infinite data definitions (e.g., lazily defined infinite streams), semantics (e.g., of concurrency), and proofs (e.g., of observational equivalence of potentially infinite processes). It is thus desirable to have good support for both induction and coinduction in systems for reasoning about programs.

The first implementations of coinduction were pioneered in Calculus of Coinductive Constructions (CIC) in the 90s, where the duality of inductive and coinductive methods was achieved by distinguishing inductive from coinductive types, recursive functions consuming inputs of inductive types from corecursive functions producing outputs of coinductive types, and inductive proof methods from coinductive proof methods.

Recently, the rapid development of automated theorem proving (ATP) has opened the way to introducing induction and coinduction to ATP. Some coinductive methods of ITP can be easily translated to ATPs. For example, definitions of (inductive and) coinductive types in ITP translate naturally into fixed-point definitions in ATP. However, some coinductive methods in ITP are much trickier to adapt to ATP: e.g., the theory of universal productivity of corecursive functions or  coinductive proof principles. 

Structural resolution is a newly introduced proof method for Horn Clause logic that can replace the classical SLD-resolution, and  promises to deliver a ``missing link” theory that merges automation of ATP and constructive coinductive methods of ITP.  In this talk I will give Type-theoretic semantics to Structural resolution, and will show how it gives rise to automated version of coinductive proofs known in CIC.     

 Joint work with John Power, Patricia Johann, Peng Fu.