Witnessing purity, constancy and mutability

Ben Lippmeier

doi:10.1007/978-3-642-10672-9_9

Witnessing purity, constancy and mutability

Ben Lippmeier^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Citations (Scopus)

Abstract

Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.

Original language	English
Title of host publication	Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings
Pages	95-110
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-10672-9_9
Publication status	Published - 2009
Event	7th Asian Symposium on Programming Languages and Systems, APLAS 2009 - Seoul, Korea, Republic of Duration: 14 Dec 2009 → 16 Dec 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5904 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th Asian Symposium on Programming Languages and Systems, APLAS 2009
Country/Territory	Korea, Republic of
City	Seoul
Period	14/12/09 → 16/12/09

Access to Document

10.1007/978-3-642-10672-9_9

Cite this

@inproceedings{27e4d5f9ab8741f590aa640ef746d1be,

title = "Witnessing purity, constancy and mutability",

abstract = "Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.",

author = "Ben Lippmeier",

year = "2009",

doi = "10.1007/978-3-642-10672-9_9",

language = "English",

isbn = "3642106714",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "95--110",

booktitle = "Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings",

note = "7th Asian Symposium on Programming Languages and Systems, APLAS 2009 ; Conference date: 14-12-2009 Through 16-12-2009",

}

Lippmeier, B 2009, Witnessing purity, constancy and mutability. in Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5904 LNCS, pp. 95-110, 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, Seoul, Korea, Republic of, 14/12/09. https://doi.org/10.1007/978-3-642-10672-9_9

Witnessing purity, constancy and mutability. / Lippmeier, Ben.
Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. 2009. p. 95-110 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5904 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Witnessing purity, constancy and mutability

AU - Lippmeier, Ben

PY - 2009

Y1 - 2009

N2 - Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.

AB - Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core language that uses dependently kinded proof witnesses to encode information about the mutability of values and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.

UR - http://www.scopus.com/inward/record.url?scp=72449198431&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-10672-9_9

DO - 10.1007/978-3-642-10672-9_9

M3 - Conference contribution

SN - 3642106714

SN - 9783642106712

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 95

EP - 110

BT - Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings

T2 - 7th Asian Symposium on Programming Languages and Systems, APLAS 2009

Y2 - 14 December 2009 through 16 December 2009

ER -

Witnessing purity, constancy and mutability

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this