Extensional universal types for call-by-value

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings
Pages122-137
Number of pages16
DOIs
Publication statusPublished - 2008 Dec 1
Externally publishedYes
Event6th Asian Symposium on Programming Languages and Systems, APLAS 2008 - Bangalore, India
Duration: 2008 Dec 92008 Dec 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5356 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)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)

Fingerprint Dive into the research topics of 'Extensional universal types for call-by-value'. Together they form a unique fingerprint.

  • Cite this

    Asada, K. (2008). Extensional universal types for call-by-value. In Programming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings (pp. 122-137). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5356 LNCS). https://doi.org/10.1007/978-3-540-89330-1-9