Abstract
Type systems hide data that is captured by function closures in function types. In most cases this is a beneficial design that enables simplicity and compositionality. However, some applications require explicit information about the data that is captured in closures.
This paper introduces open closure types, that is, function types that are decorated with type contexts. They are used to track data-flow from the environment into the function closure. A simply-typed lambda calculus is used to study the properties of the type theory of open closure types. A distinctive feature of this type theory is that an open closure type of a function can vary in different type contexts. To present an application of the type theory, it is shown that a type derivation establishes a simple non-interference property in the sense of information-flow theory. A publicly available prototype implementation of the system can be used to experiment with type derivations for example programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abel, A.: Semi-continuous Sized Types and Termination. Log. Methods Comput. Sci. 4(2) (2008)
Barthe, G., Grégoire, B., Riba, C.: Type-Based Termination with Sized Products. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 493–507. Springer, Heidelberg (2008)
Chin, W.N., Khoo, S.C.: Calculating Sized Types. High.-Ord. and Symb. Comp. 14(2-3), 261–300 (2001)
Hannan, J., Hicks, P., Liben-Nowell, D.: A Lifetime Analysis for Higher-Order Languages. Tech. rep., The Pennsylvania State University (1997), http://www.cse.psu.edu/~hannan/papers/live.ps.gz
Heintze, N., Riecke, J.G.: The SLam Calculus: Programming with Secrecy and Integrity. In: 25th Symp. on Principles of Programming Languages (POPL 1998), pp. 365–377 (1998)
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. ACM Trans. Program. Lang. Syst. (2012)
Jost, S., Hammond, K., Loidl, H.W., Hofmann, M.: Static Determination of Quantitative Resource Usage for Higher-Order Programs. In: 37th Symp. on Principles of Programming Languages (POPL 2010), pp. 223–236 (2010)
Lago, U.D., Petit, B.: The Geometry of Types. In: 40th Symp. on Principles of Programming Languages (POPL 2013), pp. 167–178 (2013)
Leroy, X.: Polymorphic Typing of an Algorithmic Language. Research report 1778, INRIA (1992)
Minamide, Y., Morrisett, J.G., Harper, R.: Typed Closure Conversion. In: 23rd Symp. on Principles of Programming Languages (POPL 1996), pp. 271–283 (1996)
Moggi, E., Taha, W., Benaissa, Z.E.-A., Sheard, T.: An idealized metaml: Simpler, and more expressive. In: 8th Europ. Symp. on Programming (ESOP 1999), pp. 193–207 (1999)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory. ACM Trans. Comput. Log. 9(3) (2008)
Petricek, T., Orchard, D., Mycroft, A.: Coeffects: Unified static analysis of context-dependence. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 385–397. Springer, Heidelberg (2013)
Pientka, B., Dunfield, J.: Programming with Proofs and Explicit Contexts. In: 10th International Conference on Principles and Practice of Declarative Programming (PPDP 2008), pp. 163–173 (2008)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Stampoulis, A., Shao, Z.: Static and User-Extensible Proof Checking. In: 39th Symp. on Principles of Programming Languages (POPL 2012), pp. 273–284 (2012)
Tsukada, T., Igarashi, A.: A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science 6(4) (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Scherer, G., Hoffmann, J. (2013). Tracking Data-Flow with Open Closure Types. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_47
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)