Jump to : Download | Abstract | See also | Keywords | Contact | BibTex reference | EndNote reference |


Michael Brandt, Fritz Henglein. Coinductive Axiomatization of Recursive Type Equality and Subtyping. In TLCA, Pages 63-81, 1997.


Download paper: Adobe portable document (pdf) pdf

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


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 characteriza- tions 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 From A, P ⊢ P infer 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 containment since no separate axiomatization of type equality is required, as in Amadio and Cardelli's axiomatization. They give rise to a natural operational interpretation of proofs as coercions. In particular, the fixpoint rule corresponds to definition by recursion. Finally, the axiomatization is closely related to (known) efficient algorithms for deciding type equality and type containment. These can be modified to not only decide type equality and type containment, but also construct proofs in our axiomatizations efficiently. In connection with the operational interpretation of proofs as coercions this gives efficient (O(n^2) time) algorithms for constructing efficient coercions from a type to any of its supertypes or isomorphic types

See also

[ tlca97 ]


[ Rectype ] [ Coinduction ]


Michael Brandt
Fritz Henglein

BibTex Reference

   Author = {Brandt, Michael and Henglein, Fritz},
   Title = {Coinductive Axiomatization of Recursive Type Equality and Subtyping},
   BookTitle = {TLCA},
   Pages = {63--81},
   Year = {1997}

EndNote Reference [help]

Get EndNote Reference (.ref)