Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68] (Theoretical Computer Science (2002) 272(1–2) (41–68), (S0304397500003479), (10.1016/S0304-3975(00)00347-9))

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

研究成果: Comment/debate

1 引用 (Scopus)

抜粋

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.

元の言語English
ページ(範囲)81-82
ページ数2
ジャーナルTheoretical Computer Science
817
DOI
出版物ステータスPublished - 2020 5 12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68] (Theoretical Computer Science (2002) 272(1–2) (41–68), (S0304397500003479), (10.1016/S0304-3975(00)00347-9))' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用