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

research-article

A theory of indirection via approximation

Authors:

Robert Dockins,

Andrew W. AppelAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 1

Pages 171 - 184

https://doi.org/10.1145/1707801.1706322

Published: 17 January 2010 Publication History

Abstract

Building semantic models that account for various kinds of indirect reference has traditionally been a difficult problem. Indirect reference can appear in many guises, such as heap pointers, higher-order functions, object references, and shared-memory mutexes.

We give a general method to construct models containing indirect reference by presenting a "theory of indirection". Our method can be applied in a wide variety of settings and uses only simple, elementary mathematics. In addition to various forms of indirect reference, the resulting models support powerful features such as impredicative quantification and equirecursion; moreover they are compatible with the kind of powerful substructural accounting required to model (higher-order) separation logic. In contrast to previous work, our model is easy to apply to new settings and has a simple axiomatization, which is complete in the sense that all models of it are isomorphic. Our proofs are machine-checked in Coq.

References

[1]

Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. Semantic foundations for typed assembly languages. ACM. Trans. on Programming Languages and Systems, 2009.

Digital Library

[2]

Amal Ahmed, Andrew W. Appel, and Roberto Virga. An indexed model of impredicative polymorphism and mutable references. http://www.cs.princeton.edu/~appel/papers/impred.pdf, January 2003.

[3]

Andrew W. Appel and Sandrine Blazy. Separation logic for small-step C minor. In 20th Int'l Conference on Theorem Proving in Higher-Order Logics (TPHOLs), pages 5--21, 2007.

Digital Library

[4]

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. Statedependent representation independence. In POPL '09: Proc. 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 340--353, 2009.

Digital Library

[5]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. A stepindexed model of substructural state. In ICFP '05: Proceedings of the tenth ACM SIGPLAN International Conference on Functional programming, pages 78--91, 2005.

Digital Library

[6]

Sten Agerholm. Domain theory in HOL. In Higher Order Logic Theorem Proving and Its Applications, LNCS, pages 295--309. Springer, 2006.

Digital Library

[7]

Amal J. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, Princeton, NJ, November 2004. Tech Report TR-713-04.

Digital Library

[8]

Andrew W. Appel, Paul-Andre Melliès, Christopher D. Richards, and Jerôme Vouillon. A very modal model of a modern, major, general type system. In Proc. 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), pages 109--122, January 2007.

Digital Library

[9]

Bodil Biering, Lars Birkedal, and Noah Torp-Smith. Bihyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29(5):24, 2007.

Digital Library

[10]

Nick Benton, Andrew Kennedy, and Carsten Varming. Some domain theory and denotational semantics in coq. In Theorem Proving in Hogher Order Logics, LNCS, pages 115--130. Springer, 2009.

Digital Library

[11]

Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. The category-theoretic solution of recursive metric-space equations. Technical report, 2009. TR-2009-119.

[12]

Nick Benton and Nicolas Tabareau. Compiling functional types to relational specifications for low level imperative code. In TLDI '09: Proc. 4th international workshop on Types in language design and implementation, pages 3--14, 2009.

Digital Library

[13]

Robert Cartwright and Derek Oppen. Unrestricted procedure calls in Hoare's logic. In POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages, pages 131--140, 1978.

Digital Library

[14]

Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS '07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pages 366--378, 2007.

Digital Library

[15]

Karl Crary. Toward a foundational typed assembly language. In POPL '03: 30th ACM Symp. on Principles of Programming Languages, pages 198--212, 2003.

Digital Library

[16]

Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical stepindexed logical relations. In Proceedings 24th Annual IEEE Symposium on Logic in Computer Science (LICS'09), 2009.

Digital Library

[17]

Robert Dockins, AndrewW. Appel, and Aquinas Hobor. Multimodal separation logic for reasoning about operational semantics. In 24th Conference on the Mathematical Foundations of Programming Semantics, pages 5--20. Springer ENTCS, 2008.

Digital Library

[18]

Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. In The 7th Asian Symposium on Programming Languages and Systems. Springer ENTCS, 2009. To appear.

Digital Library

[19]

Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. A relational modal logic for higher-order stateful adts. In POPL '10: Proc. 37th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010. To appear.

Digital Library

[20]

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In Proceedings 5th Asian Symposium on Programming Languages and Systems (APLAS'07), 2007.

Digital Library

[21]

G. Gierz, K. H. Hofmann, K. Kiemel, J. D. Lawson, M. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encylopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, UK, 2003.

[22]

Robert Harper. A simplified account of polymorphic references. Information Processing Letters, 51:201--206, 1994.

Digital Library

[23]

Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In Proc. European Symp. on Programming (ESOP 2008) (LNCS 4960), pages 353--367. Springer, 2008.

Digital Library

[24]

Aquinas Hobor. Oracle Semanatics. PhD thesis, Princeton University, Princeton, NJ, November 2008.

Digital Library

[25]

Robert Harper and Chris Stone. A type-theoretic interpretation of Standard ML. http://foxnet.cs.cmu.edu/papers/rwh-interpret.ps, 1997.

[26]

Cătălin Hritçu and Jan Schwinghammer. A step-indexed semantics of imperative objects. International Workshop on Foundations of Object-Oriented Languages (FOOL'08), 2008.

[27]

Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In POPL'06, pages 42--54, 2006.

Digital Library

[28]

Paul Blain Levy. Possible world semantics for general storage in call-by-value. In Computer Science Logic, 16th International Workshop, CSL 2002, volume 2471 of LNCS, pages 232--246, Edinburgh, Scotland, UK, September 2002. Springer.

Digital Library

[29]

Robin Milner. Logic for computable functions: description of a machine implementation. Technical report, Stanford, CA, USA, 1972.

[30]

Olaf Müller, Tobias Nipkow, David von Oheimb, and Oskar Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming, 9:191--223, 1999.

Digital Library

[31]

Tobias Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. In Computer Science Logic, volume 2471/2002 of LNCS, pages 155--182. Springer, 2002.

Digital Library

[32]

Peter W. O'Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1):271--307, May 2007.

Digital Library

[33]

David von Oheimb. Analyzing Java in Isabelle/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universität München, 2001.

[34]

Matthew Parkinson, Richard Bornat, and Cristiano Calcagno. Variables as resource in Hoare logics. Proc. of 21st Annual IEEE Symp. on Logic in Computer Science, 0:137--146, 2006.

Digital Library

[35]

David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.

[36]

Greg Restall. An Introduction to Substructural Logics. Routledge, London, England, 2000.

[37]

Thomas Schreiber. Auxiliary variables and recursive procedures. In TAPSOFT '97: Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, pages 697--711, London, UK, 1997. Springer-Verlag.

Digital Library

[38]

Norbert Schirmer. Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München, 2006.

[39]

Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994.

Digital Library

Cited By

Farka FNanevski ABanerjee ADelbianco GFábregas I(2021)On algebraic abstractions for concurrent separation logicsProceedings of the ACM on Programming Languages10.1145/34342865:POPL(1-32)Online publication date: 4-Jan-2021
https://doi.org/10.1145/3434286
Svendsen KSieczkowski FBirkedal L(2016)Transfinite Step-Indexing: Decoupling Concrete and Logical StepsProgramming Languages and Systems10.1007/978-3-662-49498-1_28(727-751)Online publication date: 2016
https://doi.org/10.1007/978-3-662-49498-1_28
Hobor AGherghina C(2012)Barriers in Concurrent Separation Logic: Now With Tool Support!Logical Methods in Computer Science10.2168/LMCS-8(2:2)20128:2Online publication date: 20-Apr-2012
https://doi.org/10.2168/LMCS-8(2:2)2012
Show More Cited By

Index Terms

A theory of indirection via approximation

Recommendations

A theory of indirection via approximation
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Building semantic models that account for various kinds of indirect reference has traditionally been a difficult problem. Indirect reference can appear in many guises, such as heap pointers, higher-order functions, object references, and shared-memory ...
Step-indexed kripke models over recursive worlds
POPL '11

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to ...
Step-indexed kripke models over recursive worlds
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 45, Issue 1

POPL '10

January 2010

500 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1707801

Issue’s Table of Contents

POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2010
520 pages
ISBN:9781605584799
DOI:10.1145/1706299
General Chair:
Manuel Hermenegildo
IMDEA-Software and T.U. of Madrid, Spain
,
Program Chair:
Jens Palsberg
UCLA, University of California, Los Angeles

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2010

Published in SIGPLAN Volume 45, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
596
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)5

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Farka FNanevski ABanerjee ADelbianco GFábregas I(2021)On algebraic abstractions for concurrent separation logicsProceedings of the ACM on Programming Languages10.1145/34342865:POPL(1-32)Online publication date: 4-Jan-2021
https://doi.org/10.1145/3434286
Svendsen KSieczkowski FBirkedal L(2016)Transfinite Step-Indexing: Decoupling Concrete and Logical StepsProgramming Languages and Systems10.1007/978-3-662-49498-1_28(727-751)Online publication date: 2016
https://doi.org/10.1007/978-3-662-49498-1_28
Hobor AGherghina C(2012)Barriers in Concurrent Separation Logic: Now With Tool Support!Logical Methods in Computer Science10.2168/LMCS-8(2:2)20128:2Online publication date: 20-Apr-2012
https://doi.org/10.2168/LMCS-8(2:2)2012
Hobor AGherghina C(2011)Barriers in Concurrent Separation LogicProgramming Languages and Systems10.1007/978-3-642-19718-5_15(276-296)Online publication date: 2011
https://doi.org/10.1007/978-3-642-19718-5_15
Beringer L(2022)Verified Software Units for Simple DFA Modules and Objects in CLeveraging Applications of Formal Methods, Verification and Validation. Software Engineering10.1007/978-3-031-19756-7_14(237-258)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19756-7_14
Farka FNanevski ABanerjee ADelbianco GFábregas I(2021)On algebraic abstractions for concurrent separation logicsProceedings of the ACM on Programming Languages10.1145/34342865:POPL(1-32)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434286
JUNG RKREBBERS RJOURDAN JBIZJAK ABIRKEDAL LDREYER D(2018)Iris from the ground up: A modular foundation for higher-order concurrent separation logicJournal of Functional Programming10.1017/S095679681800015128Online publication date: 22-Nov-2018
https://doi.org/10.1017/S0956796818000151
Cao QBeringer LGruetter SDodds JAppel A(2018)VST-FloydJournal of Automated Reasoning10.1007/s10817-018-9457-561:1-4(367-422)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-018-9457-5
Cao QCuellar SAppel A(2017)Bringing Order to the Separation Logic JungleProgramming Languages and Systems10.1007/978-3-319-71237-6_10(190-211)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_10
Svendsen KSieczkowski FBirkedal L(2016)Transfinite Step-IndexingProceedings of the 25th European Symposium on Programming Languages and Systems - Volume 963210.5555/3089528.3089556(727-751)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.5555/3089528.3089556
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents