w/in this Title
ACM SIGPLAN Notices
1-10 of 92 reviews
Proof search for propositional abstract separation logics via labelled sequents
Hóu Z., Clouston R., Goré R., Tiu A. ACM SIGPLAN Notices 49(1): 465-476, 2014. Type: Article
Pointers and sharing have always been difficult problems in program verification, and several extensions to Hoare logic have been proposed and investigated over the decades....
May 12 2014
Formal verification of object layout for C++ multiple inheritance
Ramananandro T., Dos Reis G., Leroy X. ACM SIGPLAN Notices 46(1): 67-80, 2011. Type: Article
Efficient language translation, optimized code generation, and runtime memory layout are cornerstones of modern computer language compilers. Squeezing a user’s data structures, especially with C++ multiple inheritance, into fewer but efficie...
Dec 13 2011
Specifying and verifying sparse matrix codes
Arnold G., Hölzl J., Köksal A., Bodík R., Sagiv M. ACM SIGPLAN Notices 45(9): 249-260, 2010. Type: Article
It is increasingly recognized that the heroics involved in coding efficient, low-level, imperative programs for various tasks are not sustainable. While the gain in efficiency might be quite real, the loss of certainty (with respect to correctness...
Nov 7 2011
A typed store-passing translation for general references
Pottier F. ACM SIGPLAN Notices 46(1): 147-158, 2011. Type: Article
It is a challenging task to create a well-typed semantic model for a programming language that supports references to dynamically allocated memory cells that may hold values of any type, such as functions or addresses of other cells. The essence o...
Nov 1 2011
Total parser combinators
Danielsson N. ACM SIGPLAN Notices 45(9): 285-296, 2010. Type: Article
Parser combinators are one of the best-known examples of the advantages of functional programming, as they make essential use of functions as arguments and results of functions. They are also one of the longest standing examples, going back to Bur...
Oct 13 2011
A parametric segmentation functor for fully automatic and scalable array content analysis
Cousot P., Cousot R., Logozzo F. ACM SIGPLAN Notices 46(1): 105-118, 2011. Type: Article
Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals fo...
Jun 1 2011
Regular, shape-polymorphic, parallel arrays in Haskell
Keller G., Chakravarty M., Leshchinskiy R., Peyton Jones S., Lippmeier B. ACM SIGPLAN Notices 45(9): 261-272, 2010. Type: Article
Algorithms that work on arrays are very common in science and engineering, and range from finding connected components in a graph to complex atmospheric simulations. Supporters of purely functional languages claim that these algorithms are often e...
May 18 2011
Program verification through characteristic formulae
Charguéraud A. ACM SIGPLAN Notices 45(9): 321-332, 2010. Type: Article
Charguéraud presents a tool for the verification of purely functional programs consisting of two parts. The first part is used to generate characteristic formulas, and the second part is used to formulate a set of lemmas, notations, and tacti...
Apr 18 2011
Dynamic multirole session types
Deniélou P., Yoshida N. ACM SIGPLAN Notices 46(1): 435-446, 2011. Type: Article
Session types have been introduced to provide global static descriptions of multi-process systems by specifying abstractions of the interaction patterns among a fixed set of participants. Deniélou and Yoshida’s paper extends this approa...
Apr 7 2011
Mathematizing C++ concurrency
Batty M., Owens S., Sarkar S., Sewell P., Weber T. ACM SIGPLAN Notices 46(1): 55-66, 2011. Type: Article
Integrating multi-threading into a programming language such as C++ is an error-prone task: the intuitive expectation of a “sequentially consistent” program that behaves as if concurrent memory reads and writes were put into some linea...
Apr 5 2011
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2022 ThinkLoud, Inc.