More Web Proxy on the site http://driver.im/

Article

A core calculus for scala type checking

Authors:

Vincent Cremet,

François Garillot,

Sergueï Lenglet,

Martin OderskyAuthors Info & Claims

MFCS'06: Proceedings of the 31st international conference on Mathematical Foundations of Computer Science

Pages 1 - 23

https://doi.org/10.1007/11821069_1

Published: 28 August 2006 Publication History

Abstract

We present a minimal core calculus that captures interesting constructs of the Scala programming language: nested classes, abstract types, mixin composition, and path dependent types. We show that the problems of type assignment and subtyping in this calculus are decidable.

References

[1]

P. Altherr. A Typed Intermediate Language and Algorithms for Compiling Scala by Successive Rewritings. PhD thesis, EPFL, March 2006. No. 3509.

[2]

P. Altherr and V. Cremet. Inner Classes and Virtual Types. EPFL Technical Report IC/2005/013, March 2005.

[3]

D. Ancona and E. Zucca. A primitive calculus for module systems. In Principles and Practice of Declarative Programming, LNCS 1702, 1999.

Digital Library

[4]

D. Ancona and E. Zucca. A calculus of module systems. Journal of Functional Programming, 2002.

Digital Library

[5]

G. Bracha. The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. PhD thesis, University of Utah, 1992.

Digital Library

[6]

G. Bracha and G. Lindstrom. Modularity meets inheritance. In Proceedings of the IEEE Computer Society International Conference on Computer Languages, pages 282-290, Washington, DC, 1992. IEEE Computer Society.

[7]

K. Bruce. Some challenging typing issues in object-oriented languages. In Electronic notes in Theoretical Computer Science, volume 82(8)., 2003.

[8]

K. B. Bruce, M. Odersky, and P. Wadler. A statical safe alternative to virtual types. In Proceedings of the 5th International Workshop on Foundations of Object-Oriented Languages, San Diego, USA, 1998.

[9]

K. Crary, R. Harper, and S. Puri. What is a recursive module? In SIGPLAN Conference on Programming Language Design and Implementation, pages 50-63, 1999.

Digital Library

[10]

V. Cremet. Foundations for Scala: Semantics and Proof of Virtual Types. PhD thesis, EPFL, May 2006. No. 3556.

[11]

E. Ernst. gBeta: A language with virtual attributes, block structure and propagating, dynamic inheritance. PhD thesis, Department of Computer Science, University of Aarhus, Denmark, 1999.

[12]

E. Ernst. Family polymorphism. In Proceedings of the European Conference on Object-Oriented Programming, pages 303-326, Budapest, Hungary, 2001.

Digital Library

[13]

E. Ernst, K. Ostermann, and W. Cook. A virtual class calculus. In ACM Symposium on Principles of Programming Languages (POPL'06), Jan. 2006.

Digital Library

[14]

J. Garrigue. Code reuse through polymorphic variants. In In Workshop on Foundations of Software Engineering, Sasaguri, Japan, November 2000., 2000.

[15]

R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages, January 1994.

Digital Library

[16]

T. Hirschowitz and X. Leroy. Mixin modules in a call-by-value setting. In European Symposium on Programming, pages 6-20, 2002.

Digital Library

[17]

A. Igarashi and B. C. Pierce. Foundations for virtual types. Information and Computation, 175(1):34-49, 2002.

[18]

A. Igarashi and B. C. Pierce. On inner classes. Inf. Comput., 177(1):56-89, 2002.

Digital Library

[19]

A. Igarishi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Proc. OOPSLA, Nov. 1999.

Digital Library

[20]

P. Jolly, S. Drossopoulou, C. Anderson, and K. Ostermann. Simple dependent types: Concord. In Proc. FTfJP, 2004.

[21]

X. Leroy. A syntactic theory of type generativity and sharing. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, 1994.

[22]

O.L. Madsen, B. Møller-Pedersen, and K. Nygaard. Object-Oriented Programming in the BETA Programming Language. Addison-Wesley, June 1993. ISBN0-201-62430-3.

[23]

K. Nakata, A. Ito, and J. Garrigue. Recursive object-oriented modules. In Proc. FOOL 12, Jan. 2005.

[24]

N. Nystrom, S. Chong, and A. Myers. Scalable extensibility via nested inheritance. In Proc. OOPSLA, pages 99-115, 2005.

Digital Library

[25]

M. Odersky, V. Cremet, C. Röckl, and M. Zenger. A nominal theory of objects with dependent types. In Proc. ECOOP'03, Springer LNCS, July 2003.

[26]

M. Odersky, C. Zenger, and M. Zenger. Colored local type inference. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages, pages 41- 53, January 2001.

Digital Library

[27]

M. Odersky and M. Zenger. Independently extensible solutions to the expression problem. In Proc. FOOL 12, Jan. 2005. http://homepages.inf.ed.ac.uk/ wadler/fool.

[28]

M. Odersky and M. Zenger. Scalable component abstractions. In Proc. OOPSLA, 2005.

Digital Library

[29]

B. C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131-165, July 1994.

Digital Library

[30]

B. C. Pierce and D. N. Turner. Local type inference. In Proc. POPL, 1998.

Digital Library

[31]

D. Rémy and J. Vuillon. On the (un)reality of virtual types. available from http://pauillac.inria.fr/remy/work/virtual, Mar. 2000.

[32]

M. Torgersen. Virtual types are statically safe. In 5th Workshop on Foundations of Object-Oriented Languages, San Diego, CA, USA, January 1998.

[33]

M. Torgersen. The expression problem revisited: Four new solutions using generics. In Proc. ECOOP 2004, volume 3086 of Springer LNCS, pages 123-143. Springer-Verlag, July 2004.

[34]

M. Torgersen, C. P. Hansen, E. Ernst, P. vod der Ahé, G. Bracha, and N. Gafter. Adding wildcards to the Java programming language. In Proceedings SAC'04, pages 1289-1296, Nicosia, Cyprus, Mar. 2004. ACM Press.

Digital Library

[35]

S. Zdancewic. Type inference for Java 5: Wildcards, F-bounds, and undecidability. http://www.cis.upenn.edu/~stevez/note.html, 2006.

Cited By

Martres GRichard-Foy JDoeraene S(2021)Pathless Scala: a calculus for the rest of ScalaProceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486894(12-21)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486894
Giarrusso PStefanesco LTimany ABirkedal LKrebbers R(2020)Scala step-by-step: soundness for DOT with step-indexed logical relations in IrisProceedings of the ACM on Programming Languages10.1145/34089964:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408996
Chang SBallantyne MTurner MBowman W(2019)Dependent type systems as macrosProceedings of the ACM on Programming Languages10.1145/33710714:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371071
Show More Cited By

Recommendations

Type checking and typability in domain-free lambda calculi

This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

MFCS'06: Proceedings of the 31st international conference on Mathematical Foundations of Computer Science

August 2006

813 pages

ISBN:3540377913

Editors:
Rastislav Královič
Department of Computer Science, Comenius University, Mlynská dolina, Bratislava, Slovakia
,
Paweł Urzyczyn
Institute of Informatics, University of Warsaw, Bratislava, Poland

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Martres GRichard-Foy JDoeraene S(2021)Pathless Scala: a calculus for the rest of ScalaProceedings of the 12th ACM SIGPLAN International Symposium on Scala10.1145/3486610.3486894(12-21)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1145/3486610.3486894
Giarrusso PStefanesco LTimany ABirkedal LKrebbers R(2020)Scala step-by-step: soundness for DOT with step-indexed logical relations in IrisProceedings of the ACM on Programming Languages10.1145/34089964:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408996
Chang SBallantyne MTurner MBowman W(2019)Dependent type systems as macrosProceedings of the ACM on Programming Languages10.1145/33710714:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371071
Rapoport MLhoták O(2019)A path to DOT: formalizing fully path-dependent typesProceedings of the ACM on Programming Languages10.1145/33605713:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360571
Kabir ILhoták OErdweg SOliveira B(2018)κDOT: scaling DOT with mutation and constructorsProceedings of the 9th ACM SIGPLAN International Symposium on Scala10.1145/3241653.3241659(40-50)Online publication date: 17-Sep-2018
https://dl.acm.org/doi/10.1145/3241653.3241659
Nieto AMiller HHaller PLhoták O(2017)Towards algorithmic typing for DOT (short paper)Proceedings of the 8th ACM SIGPLAN International Symposium on Scala10.1145/3136000.3136003(2-7)Online publication date: 22-Oct-2017
https://dl.acm.org/doi/10.1145/3136000.3136003
Rapoport MKabir IHe PLhoták O(2017)A simple soundness proof for dependent object typesProceedings of the ACM on Programming Languages10.1145/31338701:OOPSLA(1-27)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133870
Rapoport MLhoták O(2017)Mutable WadlerFest DOTProceedings of the 19th Workshop on Formal Techniques for Java-like Programs10.1145/3103111.3104036(1-6)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3103111.3104036
Amin NRompf T(2017)Type soundness proofs with definitional interpretersACM SIGPLAN Notices10.1145/3093333.300986652:1(666-679)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009866
Amin NRompf TCastagna GGordon A(2017)Type soundness proofs with definitional interpretersProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009866(666-679)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009866
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents