A typed lambda calculus with categorical type constructors

研究成果: Conference contribution

67 被引用数 (Scopus)

抄録

A typed lambda calculus with categorical type constructors is introduced. It has a uniform category theoretic mechanism to declare new types. Its type structure includes categorical objects like products and coproducts as well as recursive types like natural numbers and lists. It also allows duals of recursive types, i.e. lazy types, like infinite lists. It has generalized iterators for recursive types and duals of iterators for lazy types. We will give reduction rules for this simply typed lambda calculus and show that they are strongly normalizing even though it has infinite things like infinite lists.

本文言語English
ホスト出版物のタイトルCategory Theory and Computer Science, Proceedings
編集者David H. Pitt, Axel Poigne, David E. Rydeheard
出版社Springer Verlag
ページ140-157
ページ数18
ISBN(印刷版)9783540185086
DOI
出版ステータスPublished - 1987
外部発表はい
イベントInternational Conference on Category Theory and Computer Science, 1987 - Edinburgh, United Kingdom
継続期間: 1987 9 71987 9 9

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
283 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Conference

ConferenceInternational Conference on Category Theory and Computer Science, 1987
CountryUnited Kingdom
CityEdinburgh
Period87/9/787/9/9

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「A typed lambda calculus with categorical type constructors」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル