Coinductive axiomatization of recursive type equality and subtyping

• Autorzy: Brandt, M. , Henglein, F.
• Języki publikacji: EN

Abstrakty

EN

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). It states that from A,Pý P one may deduce Aý P, where P is either a type equality t = t1 or type containment t

Słowa kluczowe

EN

subtyping; type equality; recursive type; coercion; coinduction; operational interpretation; axiomatization; inference system; inference rule; fixpoint

• Czasopismo: Fundamenta Informaticae
• Rocznik: 1998
• Tom: Vol. 33, nr 4
• Strony: 309-338
• Opis fizyczny: bibliogr. 40 poz.

Twórcy

autor

Brandt, M.

autor

Henglein, F.

• Prolog Development Center A/S H.J. Holst Vej 3-5A, DK-2605 Brondby, Denmark,