Inductive-data-type systems

Frédéric Blanqui, Jean Pierre Jouannaud, Mitsuhiro Okada

Research output: Contribution to journalConference article

41 Citations (Scopus)

Abstract

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed λ-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

Original languageEnglish
Pages (from-to)41-68
Number of pages28
JournalTheoretical Computer Science
Volume272
Issue number1-2
DOIs
Publication statusPublished - 2002 Feb 6
EventTheories of Types and Proofs 1997 (TTP'97) - Tokyo, Japan
Duration: 1997 Sep 81997 Sep 18

Keywords

  • Higher-order rewriting
  • Inductive types
  • Recursive definitions
  • Strong normalization
  • Typed lambda-calculus

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Blanqui, F., Jouannaud, J. P., & Okada, M. (2002). Inductive-data-type systems. Theoretical Computer Science, 272(1-2), 41-68. https://doi.org/10.1016/S0304-3975(00)00347-9