Parametric polymorphism - universally

Neil Ghani; Fredrik Nordvall Forsberg; Federico Orsanigo

doi:10.1007/978-3-662-47709-0_7

Parametric polymorphism - universally

Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

5 Citations (Scopus)

170 Downloads (Pure)

Abstract

In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) have only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds' definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

Original language	English
Title of host publication	Logic, Language, Information, and Computation
Subtitle of host publication	22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings
Editors	Valeria de Paiva, Ruy de Queiroz, Lawrence S. Moss, Daniel Leivant, Anjolina G. de Oliveira
Pages	81-92
Number of pages	12
DOIs	https://doi.org/10.1007/978-3-662-47709-0_7
Publication status	Published - 24 Jun 2015
Event	Workshop on Logic, Language and Information (WoLLIC 2015) - Indiana University, Bloomington, IN, United States Duration: 20 Jul 2015 → 23 Jul 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Heidelberg
Volume	9160
ISSN (Print)	0302-9743

Conference

Conference	Workshop on Logic, Language and Information (WoLLIC 2015)
Country/Territory	United States
City	Bloomington, IN
Period	20/07/15 → 23/07/15

Keywords

parametric polymorphism
type theory
programming

Access to Document

10.1007/978-3-662-47709-0_7

Ghani-etal-WoLLIC-2015-Parametric-polymorphism-universallyAccepted author manuscript, 342 KB

Cite this

Ghani, N., Nordvall Forsberg, F., & Orsanigo, F. (2015). Parametric polymorphism - universally. In V. de Paiva, R. de Queiroz, L. S. Moss, D. Leivant, & A. G. de Oliveira (Eds.), Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings (pp. 81-92). (Lecture Notes in Computer Science; Vol. 9160). https://doi.org/10.1007/978-3-662-47709-0_7

Ghani, Neil ; Nordvall Forsberg, Fredrik ; Orsanigo, Federico. / Parametric polymorphism - universally. Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. editor / Valeria de Paiva ; Ruy de Queiroz ; Lawrence S. Moss ; Daniel Leivant ; Anjolina G. de Oliveira. 2015. pp. 81-92 (Lecture Notes in Computer Science).

@inproceedings{dd70f5e5661a4fd3bafc275f70c01190,

title = "Parametric polymorphism - universally",

abstract = "In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) have only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds' definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.",

keywords = "parametric polymorphism, type theory, programming",

author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Federico Orsanigo",

note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-47709-0_7; Workshop on Logic, Language and Information (WoLLIC 2015) ; Conference date: 20-07-2015 Through 23-07-2015",

year = "2015",

month = jun,

day = "24",

doi = "10.1007/978-3-662-47709-0_7",

language = "English",

isbn = "978-3-662-47708-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Heidelberg",

pages = "81--92",

editor = "{de Paiva}, Valeria and {de Queiroz}, Ruy and Moss, {Lawrence S.} and Daniel Leivant and {de Oliveira}, {Anjolina G.}",

booktitle = "Logic, Language, Information, and Computation",

}

Ghani, N , Nordvall Forsberg, F & Orsanigo, F 2015, Parametric polymorphism - universally. in V de Paiva, R de Queiroz, LS Moss, D Leivant & AG de Oliveira (eds), Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9160, pp. 81-92, Workshop on Logic, Language and Information (WoLLIC 2015), Bloomington, IN, United States, 20/07/15. https://doi.org/10.1007/978-3-662-47709-0_7

Parametric polymorphism - universally. / Ghani, Neil ; Nordvall Forsberg, Fredrik; Orsanigo, Federico.
Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. ed. / Valeria de Paiva; Ruy de Queiroz; Lawrence S. Moss; Daniel Leivant; Anjolina G. de Oliveira. 2015. p. 81-92 (Lecture Notes in Computer Science; Vol. 9160).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Parametric polymorphism - universally

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Orsanigo, Federico

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-47709-0_7

PY - 2015/6/24

Y1 - 2015/6/24

N2 - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) have only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds' definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

AB - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) have only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds' definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

KW - parametric polymorphism

KW - type theory

KW - programming

UR - http://www.indiana.edu/~iulg/wollic/

UR - http://dx.doi.org/10.1007/978-3-662-47709-0

U2 - 10.1007/978-3-662-47709-0_7

DO - 10.1007/978-3-662-47709-0_7

M3 - Conference contribution book

SN - 978-3-662-47708-3

T3 - Lecture Notes in Computer Science

SP - 81

EP - 92

BT - Logic, Language, Information, and Computation

A2 - de Paiva, Valeria

A2 - de Queiroz, Ruy

A2 - Moss, Lawrence S.

A2 - Leivant, Daniel

A2 - de Oliveira, Anjolina G.

T2 - Workshop on Logic, Language and Information (WoLLIC 2015)

Y2 - 20 July 2015 through 23 July 2015

ER -

Ghani N , Nordvall Forsberg F, Orsanigo F. Parametric polymorphism - universally. In de Paiva V, de Queiroz R, Moss LS, Leivant D, de Oliveira AG, editors, Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. 2015. p. 81-92. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-47709-0_7

Parametric polymorphism - universally

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Logical Relations for Program Verification

Universal properties for universal types in bifibrational parametricity

Cite this

Parametric polymorphism - universally

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Logical Relations for Program Verification

Research output

Universal properties for universal types in bifibrational parametricity

Cite this