Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]

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

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-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
JournalTheoretical Computer Science
DOIs
Publication statusAccepted/In press - 2018 Jan 1

Fingerprint

Abstract data types
Type Systems
Abstract Data Types
Strictly positive
Schema
Specification languages
Pattern matching
Algebraic Specification
Strong Normalization
Typed lambda Calculus
Specification Languages
Pattern Matching
Natural number
Generalise
Language
Model

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]. / Blanqui, Frédéric; Jouannaud, Jean Pierre; Okada, Mitsuhiro.

In: Theoretical Computer Science, 01.01.2018.

Research output: Contribution to journalArticle

@article{8521c7d52f49427db4afbd43c722d043,
title = "Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]",
abstract = "In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-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.",
author = "Fr{\'e}d{\'e}ric Blanqui and Jouannaud, {Jean Pierre} and Mitsuhiro Okada",
year = "2018",
month = "1",
day = "1",
doi = "10.1016/j.tcs.2018.01.010",
language = "English",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",

}

TY - JOUR

T1 - Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]

AU - Blanqui, Frédéric

AU - Jouannaud, Jean Pierre

AU - Okada, Mitsuhiro

PY - 2018/1/1

Y1 - 2018/1/1

N2 - In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-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.

AB - In a previous work (Abstract data type systems, Theoret. Comput. Sci. 173 (2) (1997)), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-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.

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

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

U2 - 10.1016/j.tcs.2018.01.010

DO - 10.1016/j.tcs.2018.01.010

M3 - Article

AN - SCOPUS:85044503356

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -