Abstract data type systems

Jean Pierre Jouannaud, Mitsuhiro Okada

研究成果: Article査読

43 被引用数 (Scopus)


This paper is concerned with the foundations of an extension of pure type systems by abstract data types, hence the name of Abstract Data Type Systems. ADTS generalize inductive types as they are defined in the calculus of constructions, by providing definitions of functions by pattern matching on the one hand, and relations among constructors of the inductive type on the other. It also generalizes the first-order framework of abstract data types by providing function types and higher-order equations. The first half of the paper describes the framework of ADTS, while the second half investigates cases where ADTS are strongly normalizing. This is shown to be the case for the polymorphic lambda calculus (with possibly subtypes) enriched by higher-order algebraic rules obeying a strong generalization of primitive recursion of higher type that we call the general schema. This covers in particular the case of inductive types whose constructors do not have functional arguments. We conjecture that this result holds true for all calculi of the so-called Barendregt's cube. On the other hand, the definition of a schema for the higher-order rules allowing for more general inductive types is left open.

ジャーナルTheoretical Computer Science
出版ステータスPublished - 1997 2月 28

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)


「Abstract data type systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。