from I - Generic separation logic
Published online by Cambridge University Press: 05 August 2014
In constructing program logics for particular applications, for particular languages, 20th-century scientists had particular difficulty with pointers—aliasing and antialiasing, updates to state, commuting of operators; and self-reference—recursive functions, recursive types, functions as first-class values, types and predicates as parameters to functions. The combination of these two was particularly difficult: pointers to mutable records that can contain pointers to function-values that operate on mutable records.
Two strains of late-20th-century logic shed light on these matters.
Girard's 1987 linear logic [43] and other substructural logics treat logical assertions as resources that can be created, consumed and (when necessary) duplicated. This kind of thinking led to the Ishtiaq/O'Hearn/Reynolds invention in 2001 of separation logic [56, 79], which is a substructural Hoare logic for reasoning about sharing and antialiasing in pointer-manipulating programs.
Scott's 1976 domain theory [84] treats data types as approximations, thereby avoiding paradoxes about recursive types and other recursive definitions/specifications: a type can be defined in terms of more approximate versions of itself, which eventually bottoms out in a type that contains no information at all. These ideas led to the Appel/McAllester/Ahmed invention in 2001 of step-indexing [10, 2] which is a kind of practical domain theory for computations on von Neumann machines.
Many 21st-century scientists have generalized these methods for application to many different program logics (and other applications); and have formalized these methods within mechanical proof assistants.
To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Find out more about the Kindle Personal Document Service.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.
To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.