469 lines
25 KiB
BibTeX
469 lines
25 KiB
BibTeX
@article{10.1145/3409006,
|
||
author = {Parreaux, Lionel},
|
||
title = {The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)},
|
||
year = {2020},
|
||
issue_date = {August 2020},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {4},
|
||
number = {ICFP},
|
||
url = {https://doi.org/10.1145/3409006},
|
||
doi = {10.1145/3409006},
|
||
abstract = {MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.},
|
||
journal = {Proc. ACM Program. Lang.},
|
||
month = {aug},
|
||
articleno = {124},
|
||
numpages = {28},
|
||
keywords = {subtyping, type inference, principal types}
|
||
}
|
||
|
||
@inproceedings{PT98,
|
||
author = {Pierce, Benjamin C. and Turner, David N.},
|
||
title = {Local type inference},
|
||
booktitle = {Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
|
||
series = {POPL '98},
|
||
year = {1998},
|
||
location = {San Diego, California, United States},
|
||
pages = {252--265}
|
||
}
|
||
|
||
@article{OZZ01,
|
||
author = "Martin Odersky and Matthias Zenger and Christoph Zenger",
|
||
title = "Colored local type inference",
|
||
journal = "Proc. 28th ACM Symposium on Principles of Programming Languages",
|
||
volume = "36",
|
||
number = "3",
|
||
pages = "41--53",
|
||
year = "2001",
|
||
xnote = "citeseer.ist.psu.edu/article/odersky01colored.html" }
|
||
|
||
|
||
@InProceedings{plue09_1,
|
||
author = {Martin Pl{\"u}micke},
|
||
title = {Java type unification with wildcards},
|
||
booktitle = {17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, W\"urzburg, Germany, October 4-6, 2007, Revised Selected Papers},
|
||
year = {2009},
|
||
editor = {Dietmar Seipel and Michael Hanus and Armin Wolf},
|
||
Volume = {5437},
|
||
publisher = {Springer-Verlag Heidelberg},
|
||
pages = {223--240},
|
||
SERIES = {Lecture Notes in Artificial Intelligence}
|
||
}
|
||
|
||
@article{DM82,
|
||
author={Luis Damas and Robin Milner},
|
||
title={Principal type-schemes for functional programs},
|
||
journal={Proc. 9th Symposium on Principles of Programming Languages},
|
||
year={1982}
|
||
}
|
||
|
||
@article{Rob65,
|
||
author={J. A. Robinson},
|
||
title={A Machine-Oriented Logic Based on the Resolution Principle},
|
||
journal={Journal of ACM},
|
||
volume={12(1)},
|
||
pages={23-41},
|
||
month=Jan,
|
||
year={1965}}
|
||
|
||
@article{MM82,
|
||
author={A. Martelli and U. Montanari},
|
||
title={An Efficient Unification Algorithm},
|
||
journal={ACM Transactions on Programming Languages and Systems},
|
||
volume={4},
|
||
pages={258-282},
|
||
year={1982}}
|
||
|
||
@InProceedings{Plue07_3,
|
||
author = {Martin Pl{\"u}micke},
|
||
title = {Typeless {P}rogramming in \textsf{{J}ava 5.0} with {W}ildcards},
|
||
booktitle = {5th {I}nternational {C}onference on {P}rinciples and {P}ractices of {P}rogramming in {J}ava},
|
||
pages = {73--82},
|
||
year = {2007},
|
||
editor = {Vasco Amaral and Lu\'is Veiga and Lu\'is Marcelino and H. Conrad Cunningham},
|
||
series = {ACM International Conference Proceeding Series},
|
||
volume = {272},
|
||
month = {September}
|
||
}
|
||
|
||
@inproceedings{plue15_2,
|
||
author = {Martin Pl{\"{u}}micke},
|
||
title = {More Type Inference in {J}ava 8},
|
||
booktitle = {Perspectives of System Informatics - 9th International Ershov Informatics
|
||
Conference, {PSI} 2014, St. Petersburg, Russia, June 24-27, 2014.
|
||
Revised Selected Papers},
|
||
editor = {Andrei Voronkov and Irina Virbitskaite},
|
||
volume = {8974},
|
||
series = {Lecture Notes in Computer Science},
|
||
pages = {248--256},
|
||
year = {2015},
|
||
publisher = {Springer}
|
||
}
|
||
|
||
@phdthesis{GS89,
|
||
author = "Gert Smolka",
|
||
title = "Logic Programming over Polymorphically Order-Sorted Types",
|
||
school = {Department Informatik, University of Kaisers\-lautern},
|
||
address = {Kaiserslautern, Germany},
|
||
month = may,
|
||
year = 1989
|
||
}
|
||
|
||
@Article{MH91,
|
||
author = "Michael Hanus",
|
||
title = "Parametric order-sorted types in logic programming",
|
||
journal = "Proc. TAPSOFT 1991",
|
||
year = "1991",
|
||
volume = "LNCS",
|
||
number = "394",
|
||
pages = "181--200"
|
||
}
|
||
|
||
@inproceedings{CB95,
|
||
author = "Christoph Beierle",
|
||
title = "Type Inferencing for Polymorphic Order-Sorted Logic Programs",
|
||
booktitle = "International Conference on Logic Programming",
|
||
pages = "765-779",
|
||
year = "1995",
|
||
OPturl = "citeseer.ist.psu.edu/beierle95type.html" }
|
||
|
||
@incollection{HiTo92,
|
||
author = {Patricia M. Hill and Rodney W. Topor},
|
||
editor = {Frank Pfenning},
|
||
title = {A {S}emantics for {T}yped {L}ogic {P}rograms},
|
||
booktitle = {Types in Logic Programming},
|
||
year = {1992},
|
||
pages = {1-62},
|
||
publisher = {MIT Press},
|
||
bibsource = {DBLP, http://dblp.uni-trier.de}
|
||
}
|
||
|
||
@inproceedings{WildFJ,
|
||
author = "Torgersen, Mads and Ernst, Erik and
|
||
Hansen, Christian Plesner",
|
||
title = "Wild {F}{J}",
|
||
booktitle = "Proceedings of FOOL 12",
|
||
year = 2005,
|
||
editor = "Wadler, Philip",
|
||
address = "Long Beach, California, USA",
|
||
month = Jan,
|
||
organization = "ACM",
|
||
publisher = "School of Informatics, University of
|
||
Edinburgh",
|
||
anote = "Electronic publication, at the URL given
|
||
below",
|
||
abstract = "This paper presents a formalization of
|
||
wildcards, which is one of the new features of
|
||
the Java programming language in version
|
||
JDK5.0. Wildcards help alleviating the
|
||
impedance mismatch between generics, or
|
||
parametric polymorphism, and traditional
|
||
object-oriented subtype polymorphism. They do
|
||
this by quantifying over parameterized types
|
||
with different type arguments. Wildcards take
|
||
inspiration from several sources including
|
||
use-site variance, and they could be considered
|
||
as a way to introduce a syntactically
|
||
light-weight kind of existential types into a
|
||
main-stream language. This formalization
|
||
describes the mechanism, in particular the
|
||
wildcard capture process where the existential
|
||
nature of wildcards becomes evident.",
|
||
url = "http://homepages.inf.ed.ac.uk/wadler/fool/",
|
||
annote = "wild-fj.pdf"
|
||
}
|
||
|
||
|
||
|
||
@inproceedings{TEP05,
|
||
author = "Torgersen, Mads and Ernst, Erik and
|
||
Hansen, Christian Plesner",
|
||
title = "Wild {F}{J}",
|
||
booktitle = "Proceedings of FOOL 12",
|
||
year = 2005,
|
||
editor = "Wadler, Philip",
|
||
address = "Long Beach, California, USA",
|
||
month = Jan,
|
||
organization = "ACM",
|
||
publisher = "School of Informatics, University of
|
||
Edinburgh",
|
||
anote = "Electronic publication, at the URL given
|
||
below",
|
||
abstract = "This paper presents a formalization of
|
||
wildcards, which is one of the new features of
|
||
the Java programming language in version
|
||
JDK5.0. Wildcards help alleviating the
|
||
impedance mismatch between generics, or
|
||
parametric polymorphism, and traditional
|
||
object-oriented subtype polymorphism. They do
|
||
this by quantifying over parameterized types
|
||
with different type arguments. Wildcards take
|
||
inspiration from several sources including
|
||
use-site variance, and they could be considered
|
||
as a way to introduce a syntactically
|
||
light-weight kind of existential types into a
|
||
main-stream language. This formalization
|
||
describes the mechanism, in particular the
|
||
wildcard capture process where the existential
|
||
nature of wildcards becomes evident.",
|
||
url = "http://homepages.inf.ed.ac.uk/wadler/fool/",
|
||
annote = "wild-fj.pdf"
|
||
}
|
||
|
||
@Article{BBDGV18,
|
||
author = {Lorenzo Bettini and Viviana Bono and Mariangiola Dezani-Ciancaglini and Paola Giannini and Betti, Venneri},
|
||
title = {Java \& Lambda: A Featherweight Story},
|
||
journal = {Logical Methods in Computer Science},
|
||
year = {2018},
|
||
OPTkey = {},
|
||
volume = {14(3:17)},
|
||
OPTnumber = {},
|
||
pages = {1--24},
|
||
OPTmonth = {},
|
||
OPTnote = {},
|
||
OPTannote = {}
|
||
}
|
||
|
||
@inproceedings{plue17_2,
|
||
author = {Pl\"{u}micke, Martin and Stadelmeier, Andreas},
|
||
title = {Introducing {S}cala-like Function Types into {J}ava-{TX}},
|
||
booktitle = {Proceedings of the 14th International Conference on Managed Languages and Runtimes},
|
||
series = {ManLang 2017},
|
||
year = {2017},
|
||
isbn = {978-1-4503-5340-3},
|
||
location = {Prague, Czech Republic},
|
||
pages = {23--34},
|
||
numpages = {12},
|
||
url_ = {http://doi.acm.org/10.1145/3132190.3132203},
|
||
doi = {10.1145/3132190.3132203},
|
||
acmid = {3132203},
|
||
publisher = {ACM},
|
||
address = {New York, NY, USA},
|
||
keywords = {Java, function types, lambda expressions, type inference},
|
||
}
|
||
|
||
@InProceedings{Plue04_1,
|
||
author = {Martin Pl{\"u}micke},
|
||
title = {Type {U}nification in \textsf{Generic--Java}},
|
||
booktitle = {Proceedings of 18th {I}nternational {W}orkshop on {U}nification ({U}{N}{I}{F}'04)},
|
||
year = {2004},
|
||
address = {Cork},
|
||
editor = {Michael Kohlhase},
|
||
month = {July},
|
||
OPturl = {http://www.lsv.ens-cachan.fr/unif/}
|
||
}
|
||
|
||
@INPROCEEDINGS{AZ04,
|
||
author = {Davide Ancona and Elena Zucca},
|
||
title = {Principal typings for {J}ava-like languages},
|
||
booktitle = {In ACM Symp. on Principles of Programming Languages 2004},
|
||
year = {2004},
|
||
pages = {306--317},
|
||
publisher = {ACM Press}
|
||
}
|
||
|
||
@inproceedings{plue16_1,
|
||
author = {Martin Pl{\"{u}}micke},
|
||
title = {Structural Type Inference in Java-like Languages},
|
||
booktitle = {Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering
|
||
2016 {(SE} 2016), Wien, 23.-26. Februar 2016.},
|
||
pages = {109--113},
|
||
year = {2016},
|
||
Optcrossref = {DBLP:conf/se/2016w},
|
||
url = {http://ceur-ws.org/Vol-1559/paper09.pdf},
|
||
timestamp = {Mon, 07 Mar 2016 13:17:33 +0100},
|
||
biburl = {http://dblp.uni-trier.de/rec/bib/conf/se/Plumicke16},
|
||
bibsource = {dblp computer science bibliography, http://dblp.org}
|
||
}
|
||
|
||
@inproceedings{ADDZ05,
|
||
author = {Ancona, Davide and Damiani, Ferruccio and Drossopoulou, Sophia and Zucca, Elena},
|
||
title = {Polymorphic Bytecode: Compositional Compilation for {J}ava-like Languages},
|
||
booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
||
series = {POPL '05},
|
||
year = {2005},
|
||
isbn = {1-58113-830-X},
|
||
location = {Long Beach, California, USA},
|
||
pages = {26--37},
|
||
numpages = {12},
|
||
url = {http://doi.acm.org/10.1145/1040305.1040308},
|
||
doi = {10.1145/1040305.1040308},
|
||
acmid = {1040308},
|
||
publisher = {ACM},
|
||
address = {New York, NY, USA},
|
||
keywords = {compositional analysis, type systems},
|
||
}
|
||
|
||
@InProceedings{aModelForJavaWithWildcards,
|
||
author="Cameron, Nicholas
|
||
and Drossopoulou, Sophia
|
||
and Ernst, Erik",
|
||
editor="Vitek, Jan",
|
||
title="A Model for Java with Wildcards",
|
||
booktitle="ECOOP 2008 -- Object-Oriented Programming",
|
||
year="2008",
|
||
publisher="Springer Berlin Heidelberg",
|
||
address="Berlin, Heidelberg",
|
||
pages="2--26",
|
||
abstract="Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.",
|
||
isbn="978-3-540-70592-5"
|
||
}
|
||
@article{WildcardsNeedWitnessProtection,
|
||
author = {Bierhoff, Kevin},
|
||
title = {Wildcards Need Witness Protection},
|
||
year = {2022},
|
||
issue_date = {October 2022},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {6},
|
||
number = {OOPSLA2},
|
||
url = {https://doi.org/10.1145/3563301},
|
||
doi = {10.1145/3563301},
|
||
abstract = {In this paper, we show that the unsoundness discovered by Amin and Tate (2016) in Java’s wildcards is avoidable, even in the absence of a nullness-aware type system. The key insight of this paper is that soundness in type systems that implicitly introduce existential types through subtyping hinges on still making sure there are suitable witness types when introducing existentially quantified type variables. To show that this approach is viable, this paper formalizes a core calculus and proves it sound. We used a static analysis based on our approach to look for potential issues in a vast corpus of Java code and found none (with 1 false positive). This confirms both that Java's unsoundness has minimal practical consequence, and that our approach can avoid it entirely with minimal false positives.},
|
||
journal = {Proc. ACM Program. Lang.},
|
||
month = {oct},
|
||
articleno = {138},
|
||
numpages = {22},
|
||
keywords = {Null, Java Wildcards, Existential Types}
|
||
}
|
||
@InProceedings{TIforFGJ,
|
||
author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
|
||
title = {{Global Type Inference for Featherweight Generic Java}},
|
||
booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)},
|
||
pages = {28:1--28:27},
|
||
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
|
||
ISBN = {978-3-95977-225-9},
|
||
ISSN = {1868-8969},
|
||
year = {2022},
|
||
volume = {222},
|
||
editor = {Ali, Karim and Vitek, Jan},
|
||
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
|
||
address = {Dagstuhl, Germany},
|
||
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16256},
|
||
URN = {urn:nbn:de:0030-drops-162560},
|
||
doi = {10.4230/LIPIcs.ECOOP.2022.28},
|
||
annote = {Keywords: type inference, Java, subtyping, generics}
|
||
}
|
||
|
||
@book{JavaLanguageSpecification,
|
||
title={The Java language specification},
|
||
author={Gosling, James},
|
||
year={2000},
|
||
publisher={Addison-Wesley Professional}
|
||
}
|
||
|
||
@inproceedings{semanticWildcardModel,
|
||
title={Towards a semantic model for Java wildcards},
|
||
author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
|
||
booktitle={Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs},
|
||
pages={1--7},
|
||
year={2010}
|
||
}
|
||
|
||
@inproceedings{addingWildcardsToJava,
|
||
title={Adding wildcards to the Java programming language},
|
||
author={Torgersen, Mads and Hansen, Christian Plesner and Ernst, Erik and Von Der Ah{\'e}, Peter and Bracha, Gilad and Gafter, Neal},
|
||
booktitle={Proceedings of the 2004 ACM symposium on Applied computing},
|
||
pages={1289--1296},
|
||
year={2004}
|
||
}
|
||
|
||
@article{TamingWildcards,
|
||
author = {Tate, Ross and Leung, Alan and Lerner, Sorin},
|
||
title = {Taming wildcards in Java's type system},
|
||
year = {2011},
|
||
issue_date = {June 2011},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {46},
|
||
number = {6},
|
||
issn = {0362-1340},
|
||
url = {https://doi.org/10.1145/1993316.1993570},
|
||
doi = {10.1145/1993316.1993570},
|
||
abstract = {Wildcards have become an important part of Java's type system since their introduction 7 years ago. Yet there are still many open problems with Java's wildcards. For example, there are no known sound and complete algorithms for subtyping (and consequently type checking) Java wildcards, and in fact subtyping is suspected to be undecidable because wildcards are a form of bounded existential types. Furthermore, some Java types with wildcards have no joins, making inference of type arguments for generic methods particularly difficult. Although there has been progress on these fronts, we have identified significant shortcomings of the current state of the art, along with new problems that have not been addressed.In this paper, we illustrate how these shortcomings reflect the subtle complexity of the problem domain, and then present major improvements to the current algorithms for wildcards by making slight restrictions on the usage of wildcards. Our survey of existing Java programs suggests that realistic code should already satisfy our restrictions without any modifications. We present a simple algorithm for subtyping which is both sound and complete with our restrictions, an algorithm for lazily joining types with wildcards which addresses some of the shortcomings of prior work, and techniques for improving the Java type system as a whole. Lastly, we describe various extensions to wildcards that would be compatible with our algorithms.},
|
||
journal = {SIGPLAN Not.},
|
||
month = {jun},
|
||
pages = {614–627},
|
||
numpages = {14},
|
||
keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
|
||
}
|
||
|
||
@inproceedings{10.1145/1449764.1449804,
|
||
author = {Smith, Daniel and Cartwright, Robert},
|
||
title = {Java type inference is broken: can we fix it?},
|
||
year = {2008},
|
||
isbn = {9781605582153},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
url = {https://doi.org/10.1145/1449764.1449804},
|
||
doi = {10.1145/1449764.1449804},
|
||
abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
|
||
booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
|
||
pages = {505–524},
|
||
numpages = {20},
|
||
keywords = {bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards},
|
||
location = {Nashville, TN, USA},
|
||
series = {OOPSLA '08}
|
||
}
|
||
|
||
|
||
|
||
@article{JavaLocalTI,
|
||
author = {Smith, Daniel and Cartwright, Robert},
|
||
title = {Java type inference is broken: can we fix it?},
|
||
year = {2008},
|
||
issue_date = {September 2008},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {43},
|
||
number = {10},
|
||
issn = {0362-1340},
|
||
url = {https://doi.org/10.1145/1449955.1449804},
|
||
doi = {10.1145/1449955.1449804},
|
||
abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
|
||
journal = {SIGPLAN Not.},
|
||
month = {oct},
|
||
pages = {505–524},
|
||
numpages = {20},
|
||
keywords = {wildcards, union types, type inference, type argument inference, subtyping, polymorphic methods, parameterized types, intersection types, generics, bounded quantification}
|
||
}
|
||
|
||
@article{FJ,
|
||
author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
|
||
title = {Featherweight Java: a minimal core calculus for Java and GJ},
|
||
year = {2001},
|
||
issue_date = {May 2001},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {23},
|
||
number = {3},
|
||
issn = {0164-0925},
|
||
url = {https://doi.org/10.1145/503502.503505},
|
||
doi = {10.1145/503502.503505},
|
||
abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
|
||
journal = {ACM Trans. Program. Lang. Syst.},
|
||
month = {may},
|
||
pages = {396–450},
|
||
numpages = {55},
|
||
keywords = {Compilation, Java, generic classes, language design, language semantics}
|
||
}
|
||
|
||
@inproceedings{principalTypes,
|
||
title={What are principal typings and what are they good for?},
|
||
author={Jim, Trevor},
|
||
booktitle={Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
|
||
pages={42--53},
|
||
year={1996}
|
||
}
|
||
|
||
@article{aNormalForm,
|
||
title={Reasoning about programs in continuation-passing style.},
|
||
author={Sabry, Amr and Felleisen, Matthias},
|
||
journal={ACM SIGPLAN Lisp Pointers},
|
||
number={1},
|
||
pages={288--298},
|
||
year={1992},
|
||
publisher={ACM New York, NY, USA}
|
||
}
|
||
|