Abstract
We define a type and effect system for a λ-calculus extended with side effects, in the form of primitives for creating and accessing resources. The analysis correctly over-approximates the sequences of resource accesses performed by a program at run-time. To accurately analyse the binding between the creation of a resource and its accesses, our system exploits a new class of types. Our ν-types have the form νN. τ ⊳ H, where the names in N are bound both in the type τ and in the effect H, that represents the sequences of resource accesses.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bartoletti, M., Degano, P., Ferrari, G.L.: History based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. To appear in ACM Tran. Progr. Lang. and Sys.
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Hard life with weak binders. In: Proc. EXPRESS (2008)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. In: Proc. Trustworthy Global Computing (2008)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: ν-types for effects and freshness analysis. Technical Report DISI-09-033, DISI - Università degli Studi di Trento (2009)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37 (1985)
Bradfield, J.: On the expressivity of the modal μ-calculus. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046. Springer, Heidelberg (1996)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: Proc. POPL (2002)
Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787. Springer, Heidelberg (1994)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proc. POPL (2008)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. POPL (2002)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoretical Computer Science 311(1-3) (2004)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1) (September 1992)
Nielson, H.R., Nielson, F.: Higher-order concurrent programs with finite communication topology. In: Proc. POPL (1994)
Odersky, M.: A functional theory of local names. In: Proc. POPL (1994)
Shinwell, M.R., Pitts, A.M., Gabbay, M.: FreshML: programming with binders made simple. In: Proc. ICFP (2003)
Skalka, C., Smith, S.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 107–128. Springer, Heidelberg (2004)
Skalka, C., Smith, S., Horn, D.V.: Types and trace effects of higher order programs. Journal of Functional Programming 18(2) (2008)
Talpin, J.-P., Jouvelot, P.: Polymorphic type, region and effect inference. Journal of Functional Programming 2(3) (1992)
Urban, C., Pitts, A.M., Gabbay, M.: Nominal unification. Theoretical Compututer Science 323(1-3) (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R. (2009). ν-Types for Effects and Freshness Analysis. In: Leucker, M., Morgan, C. (eds) Theoretical Aspects of Computing - ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science, vol 5684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03466-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-03466-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03465-7
Online ISBN: 978-3-642-03466-4
eBook Packages: Computer ScienceComputer Science (R0)