|
" Program logics for certified compilers / "
Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
661218
|
| Doc. No
|
:
|
dltt
|
| Main Entry
|
:
|
Appel, Andrew W.,1960-
|
| Title & Author
|
:
|
Program logics for certified compilers /\ Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]
|
| Page. NO
|
:
|
ix, 458 pages :: illustrations ;; 24 cm
|
| ISBN
|
:
|
9781107048010 (hardback)
|
|
|
:
|
: 110704801X (hardback)
|
| Bibliographies/Indexes
|
:
|
Includes bibliographical references and index
|
| Contents
|
:
|
Generic separation logic -- Hoare logic -- Separation logic -- Soundness of Hoare logic -- Mechanized semantic library -- Separation algebras -- Operators on separation algebras -- First-order separation logic -- A little case study -- Covariant recursive predicates -- Share accounting -- Higher order separation logic -- Separation logic as a logic -- From separation algebras to separation logic -- Simplification by rewriting -- Introduction to step-indexing -- Predicate implication and subtyping -- General recursive predicates -- Case study: separation logic with first-class functions
|
| Subject
|
:
|
Computer software-- Verification
|
| Subject
|
:
|
Logic, Symbolic and mathematical
|
| Subject
|
:
|
Compilers (Computer programs)
|
| Dewey Classification
|
:
|
005.1/4
|
| LC Classification
|
:
|
QA76.76.V47A65 2014
|
| |