Abstract
Even when programming purely mathematical functions, mutable state is often necessary to achieve good performance, as it underlies important optimisations such as path compression in union-find algorithms and memoization. Nevertheless, verified programs rarely use mutable state because of its substantial verification cost: one must either commit to a deep embedding or follow a monadic style of programming. To avoid this cost, we propose using adjustable state instead. More concretely, we extend Coq with a type of adjustable references, which are like ML references, except that the stored values are only partially observable and updatable only to values that are observationally indistinguishable from the old ones.
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.
References
Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)
Aydemir, B.E., et al.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005)
Bertot, Y.: A short presentation of Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 12–16. Springer, Heidelberg (2008)
Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234–245. ACM (2011)
Conchon, S., Filliâtre, J.-C.: A persistent union-find data structure. In: Russo, C.V., Dreyer, D. (eds.) ML 2007, pp. 37–46. ACM (2007)
Hur, C., Dreyer, D., Neis, G., Vafeiadis, V.: The marriage of bisimulations and Kripke logical relations. In: POPL 2012, pp. 59–72. ACM (2012)
Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)
Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Functional Programming 18(5-6), 865–911 (2008)
Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: POPL 2010, pp. 261–274. ACM (2010)
Pitts, A.M., Stark, I.D.B.: Operational Reasoning for Functions with Local State. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 227–273. CUP (1998)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)
Tarjan, R.E., Van Leeuwen, J.: Worst-case analysis of set union algorithms. JACM 31(2), 245–281 (1984)
Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008)
Yu, D., Shao, Z.: Verification of safety properties for concurrent assembly code. In: ICFP 2004, pp. 175–188. ACM (2004)
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
Vafeiadis, V. (2013). Adjustable References. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds) Interactive Theorem Proving. ITP 2013. Lecture Notes in Computer Science, vol 7998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39634-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-39634-2_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39633-5
Online ISBN: 978-3-642-39634-2
eBook Packages: Computer ScienceComputer Science (R0)