Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TLCA

1997

Springer

1997

Springer

We present new sound and complete axiomatizations of type equality and subtype inequality for a ﬁrst-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 ﬁxpoint rule (or coinduction principle), which has the form A, P ⊢ P A ⊢ P where P is either a type equality τ = τ′ or type containment τ ≤ τ′ . We deﬁne what it means for a proof (formal derivation) to be formally contractive and show that the ﬁxpoint 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 ﬁxpoint 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...

Related Content

Added |
08 Aug 2010 |

Updated |
08 Aug 2010 |

Type |
Conference |

Year |
1997 |

Where |
TLCA |

Authors |
Michael Brandt, Fritz Henglein |

Comments (0)