Campus Units

Computer Science

Document Type

Conference Proceeding

Conference

The 29th European Conference on Object-Oriented Programming (ECOOP’15)

Publication Version

Published Version

Publication Date

2015

Journal or Book Title

LIPIcs-Leibniz International Proceedings in Informatics

Volume

37

First Page

346

Last Page

370

DOI

10.4230/LIPIcs.ECOOP.2015.346

Conference Date

July 5-10, 2015

City

Prague, Czech Republic

Abstract

Type-and-effect systems are a powerful tool for program construction and verification. We describe intensional effect polymorphism, a new foundation for effect systems that integrates static and dynamic effect checking. Our system allows the effect of polymorphic code to be intensionally inspected through a lightweight notion of dynamic typing. When coupled with parametric polymorphism, the powerful system utilizes runtime information to enable precise effect reasoning, while at the same time retains strong type safety guarantees. We build our ideas on top of an imperative core calculus with regions. The technical innovations of our design include a relational notion of effect checking, the use of bounded existential types to capture the subtle interactions between static typing and dynamic typing, and a differential alignment strategy to achieve effi- ciency in dynamic typing. We demonstrate the applications of intensional effect polymorphism in concurrent programming, security, graphical user interface access, and memoization.

Comments

This article is published as Long, Yuheng, Yu David Liu, and Hridesh Rajan. "Intensional effect polymorphism." 29th European Conference on Object-Oriented Programming (ECOOP’15). In LIPIcs-Leibniz International Proceedings in Informatics, vol. 37. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. doi: 10.4230/LIPIcs.ECOOP.2015.346. Posted with permission.

Creative Commons License

Creative Commons Attribution 4.0 License
This work is licensed under a Creative Commons Attribution 4.0 License.

Copyright Owner

Yuheng Long and Yu David Liu and Hridesh Rajan

Language

en

File Size

application/pdf

Share

Article Location

 
COinS