Extensional universal types for call-by-value

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Citation (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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings
PublisherSpringer Verlag
Number of pages16
ISBN (Print)3540893296, 9783540893295
Publication statusPublished - 2008
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


Conference6th Asian Symposium on Programming Languages and Systems, APLAS 2008


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

Cite this