Coinductive Axiomatization of Recursive Type Equality and Subtyping

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle), which has the form A, P ⊢ P A ⊢ P where P is either a type equality τ = τ′ or type containment τ ≤ τ′ . We define what it means for a proof (formal derivation) to be formally contractive and show that the fixpoint rule is sound if the proof of the premise A, P ⊢ P is contractive. (A proof of A, P ⊢ P using the assumption axiom is, of course, not contractive.) The fixpoint rule thus allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems. The new axiomatizations are “leaner” than previous axiomatizations, particularly so for type contai...

• Type: Conference
• Year: 1997
• Where: TLCA
• Authors: Michael Brandt, Fritz Henglein
• Keywords: Theoretical Computer Science, TLCA 1997, Type Containment, Type Equality, fixpoint Rule