Abstract data type systems

Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Contribution to journalArticle

41 Citations (Scopus)

Abstract

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
Volume173
Issue number2
Publication statusPublished - 1997 Feb 28

Fingerprint

Abstract data types
Abstract Data Types
Type Systems
Schema
Calculus
Higher Order
Generalise
Higher order equation
Lambda Calculus
Pattern matching
Pattern Matching
Recursion
Regular hexahedron
Cover
First-order
Framework

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Jouannaud, J. P., & Okada, M. (1997). Abstract data type systems. Theoretical Computer Science, 173(2), 349-391.

Abstract data type systems. / Jouannaud, Jean Pierre; Okada, Mitsuhiro.

In: Theoretical Computer Science, Vol. 173, No. 2, 28.02.1997, p. 349-391.

Research output: Contribution to journalArticle

Jouannaud, JP & Okada, M 1997, 'Abstract data type systems', Theoretical Computer Science, vol. 173, no. 2, pp. 349-391.
Jouannaud JP, Okada M. Abstract data type systems. Theoretical Computer Science. 1997 Feb 28;173(2):349-391.
Jouannaud, Jean Pierre ; Okada, Mitsuhiro. / Abstract data type systems. In: Theoretical Computer Science. 1997 ; Vol. 173, No. 2. pp. 349-391.
@article{1075afa999f9437bbc438950c676739f,
title = "Abstract data type systems",
abstract = "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.",
author = "Jouannaud, {Jean Pierre} and Mitsuhiro Okada",
year = "1997",
month = "2",
day = "28",
language = "English",
volume = "173",
pages = "349--391",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Abstract data type systems

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

PY - 1997/2/28

Y1 - 1997/2/28

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0031074199&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031074199&partnerID=8YFLogxK

M3 - Article

VL - 173

SP - 349

EP - 391

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -