Abstract data type systems

Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Contribution to journalArticlepeer-review

43 Citations (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.

Original languageEnglish
Pages (from-to)349-391
Number of pages43
JournalTheoretical Computer Science
Issue number2
Publication statusPublished - 1997 Feb 28
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Abstract data type systems'. Together they form a unique fingerprint.

Cite this