Expressions, Commands, and Assertions (2002)  (Make Corrections)  
John C. Reynolds

 @ NUS   Home/Search   Context   Related

 
View or download:
cmu.edu/user/jcr/www/notes2.ps
Cached:  PS.gz  PS  PDF  Image  Update  Help

From:  cmu.edu/user/jcr/www/cs81902 (more)
(Enter author homepages)

Rate this article: (best)
  Comment on this article  
(Enter summary)

Abstract: earch of my own that is described in these lectures was supported by National Science Foundation Grant CCR{ 9804014, and by BRICS at Aarhus University. 29 References (Update)

Active bibliography (related documents):   More   All
1.7:   Separation Logic: A Logic for Shared Mutable Data Structures - Reynolds (2002)   (Correct)
1.7:   Lectures on Reasoning about Shared Mutable Data Structure Part 1 - Reynolds (2000)   (Correct)
0.8:   Intuitionistic Reasoning about Shared Mutable Data Structure - Reynolds (2000)   (Correct)

Similar documents based on text:   More   All
0.1:   Two-Categories and Program Structure - Naumann   (Correct)
0.1:   Theoretical Aspects of Object-Oriented Programming - Types.. - Gunter, (eds.) (1993)   (Correct)
0.1:   From Algol to Polymorphic Linear Lambda-calculus - O'Hearn, Reynolds (1997)   (Correct)

BibTeX entry:   (Update)

@misc{ reynolds-expressions,
  author = "John C. Reynolds",
  title = "Expressions, Commands, and Assertions",
  url = "citeseer.comp.nus.edu.sg/697389.html" }
Citations (may not include all citations):
650   An axiomatic basis for computer programming (context) - Hoare - 1969
110   BI as an assertion language for mutable data structures - Ishtiaq, O'Hearn - 2001
88   Intuitionistic reasoning about shared mutable data structure - Reynolds - 2000
82   Alias types for recursive data structures - Walker, Morrisett - 2071
58   The logic of bunched implications (context) - O'Hearn, Pym - 1999
44   Verifying properties of parallel programs: An axiomatic appr.. (context) - Owicki, Gries - 1976
43   Towards a theory of parallel programming (context) - Hoare - 1972
42   Operational reasoning for functions with local state - Pitts, Stark - 1998
41   Some techniques for proving correctness of programs which al.. (context) - Burstall - 1972
31   Proof of a program: FIND (context) - Hoare - 1971
31   Lisp and Symbolic Computation (context) - Stark, for - 1996
28   Theories of Programming Languages (context) - Reynolds - 1998
25   allocation and disposal in Hoare logic (context) - Calcagno, Ishtiaq et al. - 2000
23   Local reasoning about programs that alter data structures - O'Hearn, Reynolds et al. - 2001
23   Information and Computation (context) - Honsell, Mason et al. - 1995
20   Computability and complexity results for a spatial assertion.. - Calcagno, Yang et al. - 2001
18   Proving assertions about programs that manipulate data struc.. (context) - Oppen, Cook - 1975
17   Local Reasoning for Stateful Programs (context) - Yang - 2001
15   An assertion language for data structures (context) - Cook, Oppen - 1975
15   Lectures on reasoning about shared mutable data structure - Reynolds - 2000
14   Equivalence in functional languages with e ects (context) - Mason, Talcott - 1991
13   Theoretical Computer Science (context) - Mason, order et al. - 1997
11   Center for the Study of Language and Information (context) - Mason, of et al. - 1986
10   A semantic basis for local reasoning - Yang, O'Hearn - 2002
9   relations: Practical ways to reason about new (context) - Stark, equations - 1998
8   Reasoning about shared mutable data structure - Reynolds, O'Hearn - 2001
6   An example of local reasoning in BI pointer logic: The Schor.. - Yang - 2001
5   Veri cation of programs that destructively manipulate data (context) - Mason - 1988
5   Program logic and equivalence in the presence of garbage col.. - Calcagno, O'Hearn et al. - 2001
4   Names and Higher-Order Functions - Stark - 1994
4   Semantic and Logical Properties of Stateful Programmming - Calcagno - 2002
4   Correctness of programs manipulating data structures (context) - Kowaltowski - 1973
4   On garbage and program logic - Calcagno, O'Hearn - 2030
3   A general axiom of assignment; assignment and linked data st.. (context) - Morris - 1982
3   Program logics in the presence of garbage collection (context) - Calcagno - 2001

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.