Article

Formalization of generics for the .NET common language runtime

Authors:

Dachuan Yu,

Andrew Kennedy,

Don SymeAuthors Info & Claims

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 39 - 51

https://doi.org/10.1145/964001.964005

Published: 01 January 2004 Publication History

Get Access

Abstract

We present a formalization of the implementation of generics in the .NET Common Language Runtime (CLR), focusing on two novel aspectsof the implementation: mixed specialization and sharing, and efficient support for run-time types. Some crucial constructs used in the implementation are dictionaries and run-time type representations. We formalize these aspects type-theoretically in a way that corresponds in spirit to the implementation techniques used in practice. Both the techniques and the formalization also help us understand the range of possible implementation techniques for other languages, e.g., ML, especially when additional source language constructs such as run-time types are supported. A useful by-product of this study is a type system for a subset of the polymorphic IL proposed for the .NET CLR.

References

[1]

O. Agesen, S. N. Freund, and J. C. Mitchell. Adding parameterized types to Java. In Object-Oriented Programming: Systems, Languages and Applications (OOPSLA), October 1997.

Digital Library

Google Scholar

[2]

P. N. Benton, A. J. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In 3rd ACM SIGPLAN International Conference on Functional Programming, September 1998.

Digital Library

Google Scholar

[3]

G. Bracha, M. Odersky, D. Stoutamire, and P. Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Object-Oriented Programming: Systems, Languages, Applications (OOPSLA), October 1998.

Digital Library

Google Scholar

[4]

R. Cartwright and G. L. Steele. Compatible genericity with run-time types for the Java programming language. In Object-Oriented Programming: Systems, Languages, Applications (OOPSLA), October 1998.

Digital Library

Google Scholar

[5]

K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In International Conference on Functional Programming, pages 301--312. ACM Press, Sept. 1998.

Digital Library

Google Scholar

[6]

Ecma International. ECMA and ISO C# and Common Language Infrastructure standards. See http://msdn.microsoft.com/net/ecma/.

Google Scholar

[7]

A. Gordon and D. Syme. Typing a multi-language intermediate code. In 27th Annual ACM Symposium on Principles of Programming Languages, January 2001.

Digital Library

Google Scholar

[8]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification (Second Edition). Addison-Wesley, 2000.

Digital Library

Google Scholar

[9]

R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proceedings of the Symposium on Principles of Programming Languages, pages 130--141, San Francisco, California, Jan. 1995. ACM Press.

Digital Library

Google Scholar

[10]

A. Hejlsberg. The csharp programming language. Invited talk at Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2002.

Google Scholar

[11]

A. Hejlsberg and S. Wiltamuth. C# 2.0 language reference. See http://msdn.microsoft.com/vcsharp/.

Google Scholar

[12]

A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 1999.

Digital Library

Google Scholar

[13]

A. Jeffrey. Generic Java type inference is unsound. The Types Forum, December 2001.

Google Scholar

[14]

A. J. Kennedy and D. Syme. Design and implementation of generics for the .NET Common Language Runtime. In Programming Language Design and Implementation. ACM, 2001.

Digital Library

Google Scholar

[15]

A. J. Kennedy and D. Syme. Transposing F to C#: Expressivity of parametric polymorphism in an object-oriented language. In Concurrency and Computation: Practice and Experience, to appear.

Digital Library

Google Scholar

[16]

X. Leroy. Unboxed objects and polymorphic typing. In 19th symposium Principles of Programming Languages, pages 177--188. ACM Press, 1992.

Digital Library

Google Scholar

[17]

T. Lindholm and F. Yellin. The Java Virtual Machine Specification (Second Edition). Addison-Wesley, 1999.

Digital Library

Google Scholar

[18]

Microsoft Corporation. The .NET Common Language Runtime. See http://msdn.microsoft.com/net/.

Google Scholar

[19]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In 25th ACM Symposium on Principles of Programming Languages, pages 85--97. ACM Press, Jan. 1998.

Digital Library

Google Scholar

[20]

A. C. Myers, J. A. Bank, and B. Liskov. Parameterized types for java. In 24th ACM Symposium on Principles of Programming Languages, pages 132--145, January 1997.

Digital Library

Google Scholar

[21]

M. Odersky, E. Runne, and P. Wadler. Two ways to bake your Pizza -- translating parameterised types into Java. Technical Report CIS-97-016, University of South Australia, 1997.

Google Scholar

[22]

M. Odersky and P. Wadler. Pizza into Java: Translating theory into practice. In Proc. 24th ACM Symposium on Principles of Programming Languages, January 1997.

Digital Library

Google Scholar

[23]

K. Palacz and J. Vitek. Subtype tests in real time. In European Conference on Object Oriented Programming, 2003.

Google Scholar

[24]

B. Saha and Z. Shao. Optimal type lifting. In Types in Compilation Workshop, pages 156--177, Kyoto, Japan, March 1998.

Digital Library

Google Scholar

[25]

Z. Shao. Flexible representation analysis. In Proc. 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP'97), pages 85--98, Amsterdam, The Netherlands, June 1997.

Digital Library

Google Scholar

[26]

Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation, June 1997.

Google Scholar

[27]

M. Viroli and A. Natali. Parametric polymorphism in Java: an approach to translation based on reflective features. In Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). ACM, October 2000.

Digital Library

Google Scholar

[28]

D. Yu, A. Kennedy, and D. Syme. Formalization of generics for the .NET Common Language Runtime. Technical report, Microsoft Research, 2003. To appear.

Google Scholar

[29]

D. Yu, V. Trifonov, and Z. Shao. Type-preserving compilation of Featherweight IL. In Proc. 2002 Workshop on Formal Techniques for Java-like Programs (FTfJP'02), June 2002.

Digital Library

Google Scholar

Cited By

View all

Ellis SZhu SYoshida NSong L(2022)Generic go to go: dictionary-passing, monomorphisation, and hybridProceedings of the ACM on Programming Languages10.1145/35633316:OOPSLA2(1207-1235)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563331
Griesemer RHu RKokke WLange JTaylor IToninho BWadler PYoshida N(2020)Featherweight goProceedings of the ACM on Programming Languages10.1145/34282174:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428217
Ureche VStojanovic MBeguet RStucki NOdersky MStansifer RKrall A(2015)Improving the Interoperation between Generics TranslationsProceedings of the Principles and Practices of Programming on The Java Platform10.1145/2807426.2807436(113-124)Online publication date: 8-Sep-2015
https://dl.acm.org/doi/10.1145/2807426.2807436
Show More Cited By

Index Terms

Formalization of generics for the .NET common language runtime
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
    2. General programming languages
      1. Language features
        Classes and objects
        Polymorphism
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

Design and implementation of generics for the .NET Common language runtime
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

The Microsoft.NET Common Language Runtime provides a shared type system, intermediate language and dynamic execution environment for the implementation and inter-operation of multiple source languages. In this paper we extend it with direct support for ...
Formalization of generics for the .NET common language runtime
POPL '04

We present a formalization of the implementation of generics in the .NET Common Language Runtime (CLR), focusing on two novel aspectsof the implementation: mixed specialization and sharing, and efficient support for run-time types. Some crucial ...
Towards proving type safety of .NET CIL

A crucial role in the Microsoft .NET Framework Common Language Runtime (CLR) security model is played by type safety of the Common Intermediate Language (CIL). In this paper, we formally prove type safety of a large subset of CIL. To do so, we begin by ...

Reviews

Reviewer: Marlin W Thomas

Two fundamental parts of the .NET framework are the common language runtime (CLR) environment and the base class libraries (BCL). The CLR is the execution environment for all languages in the .NET framework. CLR, in a model similar to that of the Java virtual machine, reads Microsoft intermediate language (IL) code generated by a .NET compiler. The BCL provides prewritten services that are available to clients. The authors formalize the implementation of generics in the CLR. They provide, using operational semantics, a syntax of the purely functional core of IL, called baby IL with generics (BILG), its typing and evaluation rules, and class and method typing in BILG. They use highly developed type theories to organize and generate their work. The use of BILG, a miniature form of generic IL, helps the authors in presenting the essential features of generic IL. The paper, which is directed toward programming language specialists, provides a deeper understanding of the status of types in the CLR. Readers with a background in semantics and type theory will find this piece especially helpful in grasping generics in the CLR. Because of the broad applicability of the CLR, any fuller understanding of generics helps developers and computer scientists better develop programs for the .NET framework, which is likely to become an industry standard. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2004

364 pages

ISBN:158113729X

DOI:10.1145/964001

General Chair:
Neil D. Jones
DIKU, University of Copenhagen
,
Program Chair:
Xavier Leroy
INRIA Rocquencourt

ACM SIGPLAN Notices Volume 39, Issue 1
POPL '04
January 2004
352 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/982962
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2004

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL04

Sponsor:

POPL04: The 31st Annual ACM Symposium on Principles of Programming Languages

January 14 - 16, 2004

Venice, Italy

Acceptance Rates

POPL '04 Paper Acceptance Rate 29 of 176 submissions, 16%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
1,069
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ellis SZhu SYoshida NSong L(2022)Generic go to go: dictionary-passing, monomorphisation, and hybridProceedings of the ACM on Programming Languages10.1145/35633316:OOPSLA2(1207-1235)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563331
Griesemer RHu RKokke WLange JTaylor IToninho BWadler PYoshida N(2020)Featherweight goProceedings of the ACM on Programming Languages10.1145/34282174:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428217
Ureche VStojanovic MBeguet RStucki NOdersky MStansifer RKrall A(2015)Improving the Interoperation between Generics TranslationsProceedings of the Principles and Practices of Programming on The Java Platform10.1145/2807426.2807436(113-124)Online publication date: 8-Sep-2015
https://dl.acm.org/doi/10.1145/2807426.2807436
Ureche VBurmako EOdersky M(2014)Late data layoutACM SIGPLAN Notices10.1145/2714064.266019749:10(397-416)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2714064.2660197
Ureche VBurmako EOdersky MBlack AMillstein T(2014)Late data layoutProceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications10.1145/2660193.2660197(397-416)Online publication date: 15-Oct-2014
https://dl.acm.org/doi/10.1145/2660193.2660197
Sallenave ODucournau R(2012)Lightweight generics in embedded systems through static analysisACM SIGPLAN Notices10.1145/2345141.224842147:5(11-20)Online publication date: 12-Jun-2012
https://dl.acm.org/doi/10.1145/2345141.2248421
Sallenave ODucournau RWilhelm RFalk HYi W(2012)Lightweight generics in embedded systems through static analysisProceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems10.1145/2248418.2248421(11-20)Online publication date: 12-Jun-2012
https://dl.acm.org/doi/10.1145/2248418.2248421
Klein CFlatt MFindler R(2012)The Racket virtual machine and randomized testingHigher-Order and Symbolic Computation10.1007/s10990-013-9091-125:2-4(209-253)Online publication date: 1-Dec-2012
https://dl.acm.org/doi/10.1007/s10990-013-9091-1
Wehr SThiemann P(2011)JavaGIACM Transactions on Programming Languages and Systems10.1145/1985342.198534333:4(1-83)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1145/1985342.1985343
Bierman GMeijer ETorgersen M(2010)Adding dynamic types to CProceedings of the 24th European conference on Object-oriented programming10.5555/1883978.1883986(76-100)Online publication date: 21-Jun-2010
https://dl.acm.org/doi/10.5555/1883978.1883986
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Design and implementation of generics for the .NET Common language runtime