A generic type-and-effect system

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A generic type-and-effect system

Full text

Pdf (468 KB)

Source

Types In Languages Design And Implementation archive
Proceedings of the 4th international workshop on Types in language design and implementation table of contents

Savannah, GA, USA

SESSION: Session 2 table of contents

Pages 39-50

Year of Publication: 2009

ISBN:978-1-60558-420-1

Authors

Daniel Marino	University of California, Los Angeles, Los Angeles, CA, USA
Todd Millstein	University of California, Los Angeles, Los Angeles, CA, USA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 69, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1481861.1481868 What is a DOI?

ABSTRACT

Type-and-effect systems are a natural approach for statically reasoning about a program's execution. They have been used to track a variety of computational effects, for example memory manipulation, exceptions, and locking. However, each type-and-effect system is typically implemented as its own monolithic type system that hard-codes a particular syntax of effects along with particular rules to track and control those effects.

We present a generic type-and-effect system, which is parameterized by the syntax of effects to track and by two functions that together specify the effect discipline to be statically enforced. We describe how a standard form of type soundness is ensured by requiring these two functions to obey a few natural monotonicity requirements. We demonstrate that several effect systems from the literature can be viewed as instantiations of our generic type system. Finally, we describe the implementation of our type-and-effect system and mechanically checked type soundness proof in the Twelf proof assistant.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006 [doi>10.1145/1119479.1119480]
	2	Martín Abadi , Andrew Birrell , Tim Harris , Michael Isard, Semantics of transactional memory and automatic mutual exclusion, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
	3	Nick Benton , Peter Buchlovsky, Semantics of an effect analysis for exceptions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190320]
	4	Nick Benton, Andrew Kennedy, Martin Hofmann, and Lennart Beringer. Reading, writing and relations: Towards extensional semantics for effect analyses. In Programming Languages and Systems, 4th Asian Symposium (APLAS 2006), pages 114--130. Springer, 2006.
	5	Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
	6	Brian Chin, Shane Markstrum, Todd Millstein, and Jens Palsberg. Inference of user-defined type qualifiers and qualifier rules. In European Symposium on Programming, 2006.
	7	Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
	8	Linda DeMichiel. Enterprise JavaBeans Specification, Version 3.0. SUN Microsystems, 2004.
	9	Andrzej Filinski, Representing layered monads, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.175-188, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292557]
	10	Jeffrey Fischer , Rupak Majumdar , Todd Millstein, Tasks: language support for event-driven programming, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France [doi>10.1145/1244381.1244403]
	11	Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
	12	Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
	13	Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	14	Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006 [doi>10.1145/1186632.1186635]
	15	David K. Gifford , John M. Lucassen, Integrating functional and imperative programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.28-38, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319848]
	16	David K. Gifford, Pierre Jouvelot, Mark A. Sheldon, and James W. O'Toole. Report on the FX-91 programming language. Technical Report MIT/LCS/TR-531, MIT Laboratory for Computer Science, 1992.
	17	James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	18	Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
	19	Michael Isard , Andrew Birrell, Automatic mutual exclusion, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
	20	Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
	21	Milo Martin , Colin Blundell , E. Lewis, Subtleties of Transactional Memory Atomicity Semantics, IEEE Computer Architecture Letters, v.5 n.2, p.17, July 2006 [doi>10.1109/L-CA.2006.18]
	22	E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
	23	Aleksandar Nanevski, From dynamic binding to state via modal possibility, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.207-218, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888271]
	24	Aleksandar Nanevski. A modal calculus for exception handling. In Intuitionistic Modal Logics and Applications Workshop, 2005.
	25	Iulian Neamtiu , Michael Hicks , Jeffrey S. Foster , Polyvios Pratikakis, Contextual effects for version-consistent dynamic software updating and safe concurrent programming, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
	26	P. Ørbæk , J. Palsberg, Trust in the λ-calculus, Journal of Functional Programming, v.7 n.6, p.557-591, November 1997 [doi>10.1017/S0956796897002906]
	27	Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
	28	Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
	29	Umesh Shankar , Kunal Talwar , Jeffrey S. Foster , David Wagner, Detecting format string vulnerabilities with type qaualifiers, Proceedings of the 10th conference on USENIX Security Symposium, p.16-16, August 13-17, 2001, Washington, D.C.
	30	Rob Simmons. Twelf as a unified framework for language formalization and implementation, 2005. URL http://www.cs.princeton.edu/~rsimmons/thesis.pdf. Undergraduate honors thesis, Princeton University.
	31	Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3): 245--271, 1992.
	32	Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177855]
	33	Philip Wadler , Peter Thiemann, The marriage of effects and monads, ACM Transactions on Computational Logic (TOCL), v.4 n.1, p.1-32, January 2003 [doi>10.1145/601775.601776]
	34	David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]
	35	Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]