Vladimir Komendantsky: A method of nested induction-coinduction illustrated on recursive subtyping.
I am interested in certian kinds of subtype and containment relations and
their decision algorithms. A formal definition of a relation is required in a
theorem prover, for example, for establishing a verified soundness and
completeness result for a decision algorithm. In the talk, I describe a
formalisation of a recursive subtype relation by using a method of nested
induction-coinduction in the proof assistant Coq. Thus the subtype relation is
not merely a semantic relation on tree interpretations of types, but the
required syntactic relation on types.