Type checking for JavaScript

Christopher Anderson; Paola Giannini

doi:10.1016/j.entcs.2005.09.010

Type checking for JavaScript

Christopher Anderson
, Paola Giannini

Department of Sustainable Development and Ecological Transition

Research output: Contribution to journal › Conference article › peer-review

Abstract

JavaScript is a powerful imperative object based language made popular by its use in web pages. It supports flexible program development by allowing dynamic addition of members to objects. Code is dynamically typed: a runtime access to a non-existing member causes an error. We suggest a static type system for JavaScript that will detect such type errors. Therefore, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. We demonstrate our type system with a formalism of JavaScript, JS₀. Our types are structural. Members of an object type are classified into definite and potential. A potential member becomes definite upon assignment. We outline a proof that our type system is sound.

Original language	English
Pages (from-to)	37-58
Number of pages	22
Journal	Electronic Notes in Theoretical Computer Science
Volume	138
Issue number	2
DOIs	https://doi.org/10.1016/j.entcs.2005.09.010
Publication status	Published - 23 Nov 2005
Event	Proceedings of the Second Workshop on Object Oriented Developments (WOOD 2004) - Duration: 30 Aug 2004 → 30 Aug 2004

Keywords

JavaScript
Scripting Languages
Structural Recursive Types
Type Checking

Access to Document

10.1016/j.entcs.2005.09.010

Cite this

@article{893eab1b30114a42a5ea2bf9dc101336,

title = "Type checking for JavaScript",

abstract = "JavaScript is a powerful imperative object based language made popular by its use in web pages. It supports flexible program development by allowing dynamic addition of members to objects. Code is dynamically typed: a runtime access to a non-existing member causes an error. We suggest a static type system for JavaScript that will detect such type errors. Therefore, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. We demonstrate our type system with a formalism of JavaScript, JS0. Our types are structural. Members of an object type are classified into definite and potential. A potential member becomes definite upon assignment. We outline a proof that our type system is sound.",

keywords = "JavaScript, Scripting Languages, Structural Recursive Types, Type Checking",

author = "Christopher Anderson and Paola Giannini",

note = "Funding Information: 1 Work partly supported by DART, European Commission Research Directorates, IST-01-6-1A 2 MURST Cofin{\textquoteright}02 project McTati 3 Email: [email protected] 4 Email: [email protected]; Proceedings of the Second Workshop on Object Oriented Developments (WOOD 2004) ; Conference date: 30-08-2004 Through 30-08-2004",

year = "2005",

month = nov,

day = "23",

doi = "10.1016/j.entcs.2005.09.010",

language = "English",

volume = "138",

pages = "37--58",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "2",

}

TY - JOUR

T1 - Type checking for JavaScript

AU - Anderson, Christopher

AU - Giannini, Paola

N1 - Funding Information: 1 Work partly supported by DART, European Commission Research Directorates, IST-01-6-1A 2 MURST Cofin’02 project McTati 3 Email: [email protected] 4 Email: [email protected]

PY - 2005/11/23

Y1 - 2005/11/23

N2 - JavaScript is a powerful imperative object based language made popular by its use in web pages. It supports flexible program development by allowing dynamic addition of members to objects. Code is dynamically typed: a runtime access to a non-existing member causes an error. We suggest a static type system for JavaScript that will detect such type errors. Therefore, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. We demonstrate our type system with a formalism of JavaScript, JS0. Our types are structural. Members of an object type are classified into definite and potential. A potential member becomes definite upon assignment. We outline a proof that our type system is sound.

AB - JavaScript is a powerful imperative object based language made popular by its use in web pages. It supports flexible program development by allowing dynamic addition of members to objects. Code is dynamically typed: a runtime access to a non-existing member causes an error. We suggest a static type system for JavaScript that will detect such type errors. Therefore, programmers can benefit from the flexible programming style offered by JavaScript and from the safety offered by a static type system. We demonstrate our type system with a formalism of JavaScript, JS0. Our types are structural. Members of an object type are classified into definite and potential. A potential member becomes definite upon assignment. We outline a proof that our type system is sound.

KW - JavaScript

KW - Scripting Languages

KW - Structural Recursive Types

KW - Type Checking

UR - https://www.scopus.com/pages/publications/27744498729

U2 - 10.1016/j.entcs.2005.09.010

DO - 10.1016/j.entcs.2005.09.010

M3 - Conference article

AN - SCOPUS:27744498729

SN - 1571-0661

VL - 138

SP - 37

EP - 58

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

T2 - Proceedings of the Second Workshop on Object Oriented Developments (WOOD 2004)

Y2 - 30 August 2004 through 30 August 2004

ER -

Type checking for JavaScript

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this