Coverart for item
The Resource Program logics for certified compilers, Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]

Program logics for certified compilers, Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]

Label
Program logics for certified compilers
Title
Program logics for certified compilers
Statement of responsibility
Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]
Creator
Author
Subject
Language
eng
Cataloging source
DLC
http://library.link/vocab/creatorDate
1960-
http://library.link/vocab/creatorName
Appel, Andrew W.
Illustrations
illustrations
Index
index present
Literary form
non fiction
Nature of contents
bibliography
http://library.link/vocab/subjectName
  • Computer software
  • Logic, Symbolic and mathematical
  • Compilers (Computer programs)
Label
Program logics for certified compilers, Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier MARC source
rdacarrier
Content category
text
Content type MARC source
rdacontent
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 -- Data structures in indirection theory -- Applying higher-order separation logic -- Lifted seaparation logics -- Separation Logic for CompCert -- Verifiable C -- Expressions, values, and assertions -- The VST separation logic for C light -- Typechecking for verifiable C -- Derived rules and proof automation for C LIght -- Proof of a program -- More C programs -- Dependently typed C programs -- Concurrent separation logic -- Operational semantics of CompCert -- CompCert -- The CompCert memory model -- How to specify a compiler -- C light operational semantics -- Higher-order semantic models -- Indirection theory -- Case study: Lambda-calculus with references -- Higher-order Hoare logic -- Higher-order separation logic -- Semantic models of predicates-in-the-heap -- Semantic model and soundness of verifiable C -- Separation algebra for CompCert -- Share models -- Juicy memories -- Modeling the Hoare judgment -- Semantic model of CSL -- Modular structure of the development -- Applications -- Foundational static analysis -- Heap theorem prover
Control code
ocn869460543
Dimensions
24 cm
Extent
ix, 458 pages:
Isbn
9781107048010
Isbn Type
(hardback)
Lccn
2014001794
Media category
unmediated
Media MARC source
rdamedia
Other physical details
illustrations
System control number
(OCoLC)869460543
Label
Program logics for certified compilers, Andrew W. Appel, Princeton University, Princeton, New Jersey ... [and seven others]
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
volume
Carrier MARC source
rdacarrier
Content category
text
Content type MARC source
rdacontent
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 -- Data structures in indirection theory -- Applying higher-order separation logic -- Lifted seaparation logics -- Separation Logic for CompCert -- Verifiable C -- Expressions, values, and assertions -- The VST separation logic for C light -- Typechecking for verifiable C -- Derived rules and proof automation for C LIght -- Proof of a program -- More C programs -- Dependently typed C programs -- Concurrent separation logic -- Operational semantics of CompCert -- CompCert -- The CompCert memory model -- How to specify a compiler -- C light operational semantics -- Higher-order semantic models -- Indirection theory -- Case study: Lambda-calculus with references -- Higher-order Hoare logic -- Higher-order separation logic -- Semantic models of predicates-in-the-heap -- Semantic model and soundness of verifiable C -- Separation algebra for CompCert -- Share models -- Juicy memories -- Modeling the Hoare judgment -- Semantic model of CSL -- Modular structure of the development -- Applications -- Foundational static analysis -- Heap theorem prover
Control code
ocn869460543
Dimensions
24 cm
Extent
ix, 458 pages:
Isbn
9781107048010
Isbn Type
(hardback)
Lccn
2014001794
Media category
unmediated
Media MARC source
rdamedia
Other physical details
illustrations
System control number
(OCoLC)869460543

Library Locations

    • Albany LibraryBorrow it
      Gate 1, East Precinct, Albany Expressway (SH17), Albany, Auckland, 0632, NZ
      -36.733330 174.700641
Processing Feedback ...