A computation model for executable higher-order algebraic specification languages

Jean Pierre Jouannaud, Mitsuhiro Okada

研究成果: Conference contribution

88 被引用数 (Scopus)

抄録

The combination of (polymorphically) typed lambda-calculi with first-order as well as higher-order rewrite rules is considered. The need of such a combination for exploiting the benefits of algebraically defined data types within functional programming is demonstrated. A general modularity result, which allows as particular cases primitive recursive functionals of higher types, transfinite recursion of higher types, and inheritance for all types, is proved. The class of languages considered is first defined, and it is shown how to reduce the Church-Rosser and termination (also called strong normalization) properties of an algebraic functional language to a so-called principal lemma whose proof depends on the property to be proved and on the language considered. The proof of the principal lemma is then sketched for various languages. The results allows higher order rules defining the higher-order constants by a certain generalization of primitive recursion. A prototype of such primitive recursive definitions is provided by the definition of the map function for lists.

本文言語English
ホスト出版物のタイトルProceedings - Symposium on Logic in Computer Science
出版社Publ by IEEE
ページ350-361
ページ数12
ISBN(印刷版)081862230X
出版ステータスPublished - 1991 7月 1
外部発表はい
イベントProceedings of the 6th Annual IEEE Symposium on Logic in Computer Science - Amsterdam, Neth
継続期間: 1991 7月 151991 7月 18

出版物シリーズ

名前Proceedings - Symposium on Logic in Computer Science

Other

OtherProceedings of the 6th Annual IEEE Symposium on Logic in Computer Science
CityAmsterdam, Neth
Period91/7/1591/7/18

ASJC Scopus subject areas

  • ソフトウェア
  • 数学 (全般)

フィンガープリント

「A computation model for executable higher-order algebraic specification languages」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル