Extensional universal types for call-by-value

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

We propose -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types are genuinely right adjoint to the weakening, i.e., β-equality and η-equality hold for not only values but all terms. We give monadic style categorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we construct concrete models for the calculus in a generic manner, exploiting "relevant" parametricity. On such models, we can obtain a reasonable class of monads consistent with extensional universal types. This class admits polynomial-like constructions, and includes non-termination, exception, global state, input/output, and list-non-determinism.

本文言語English
ホスト出版物のタイトルProgramming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings
ページ122-137
ページ数16
DOI
出版ステータスPublished - 2008 12 1
外部発表はい
イベント6th Asian Symposium on Programming Languages and Systems, APLAS 2008 - Bangalore, India
継続期間: 2008 12 92008 12 11

出版物シリーズ

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

Conference

Conference6th Asian Symposium on Programming Languages and Systems, APLAS 2008
CountryIndia
CityBangalore
Period08/12/908/12/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「Extensional universal types for call-by-value」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル