Why Separation Logic Works.
Saved in:
| Title: | Why Separation Logic Works. |
|---|---|
| Authors: | Pym, David1 d.pym@ucl.ac.uk, Spring, Jonathan M.1 jspring@cs.ucl.ac.uk, O'Hearn, Peter1 p.ohearn@ucl.ac.uk |
| Source: | Philosophy & Technology. Sep2019, Vol. 32 Issue 3, p483-516. 34p. |
| Subject Terms: | *Computer software, Computer logic, Software engineering, Nonrenewable natural resources, Logic, Proof theory |
| Abstract: | One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer's conceptual model of a program's manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field. [ABSTRACT FROM AUTHOR] |
| Copyright of Philosophy & Technology is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Education Research Complete |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: ehh DbLabel: Education Research Complete An: 138108665 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Why Separation Logic Works. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Pym%2C+David%22">Pym, David</searchLink><relatesTo>1</relatesTo><i> d.pym@ucl.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Spring%2C+Jonathan+M%2E%22">Spring, Jonathan M.</searchLink><relatesTo>1</relatesTo><i> jspring@cs.ucl.ac.uk</i><br /><searchLink fieldCode="AR" term="%22O'Hearn%2C+Peter%22">O'Hearn, Peter</searchLink><relatesTo>1</relatesTo><i> p.ohearn@ucl.ac.uk</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Philosophy+%26+Technology%22">Philosophy & Technology</searchLink>. Sep2019, Vol. 32 Issue 3, p483-516. 34p. – Name: Subject Label: Subject Terms Group: Su Data: *<searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+logic%22">Computer logic</searchLink><br /><searchLink fieldCode="DE" term="%22Software+engineering%22">Software engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Nonrenewable+natural+resources%22">Nonrenewable natural resources</searchLink><br /><searchLink fieldCode="DE" term="%22Logic%22">Logic</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer's conceptual model of a program's manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to (a subset of) the problems, process, and results of computer scientists for those outside the field. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Philosophy & Technology is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=ehh&AN=138108665 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s13347-018-0312-8 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 34 StartPage: 483 Subjects: – SubjectFull: Computer software Type: general – SubjectFull: Computer logic Type: general – SubjectFull: Software engineering Type: general – SubjectFull: Nonrenewable natural resources Type: general – SubjectFull: Logic Type: general – SubjectFull: Proof theory Type: general Titles: – TitleFull: Why Separation Logic Works. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Pym, David – PersonEntity: Name: NameFull: Spring, Jonathan M. – PersonEntity: Name: NameFull: O'Hearn, Peter IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 09 Text: Sep2019 Type: published Y: 2019 Identifiers: – Type: issn-print Value: 22105433 Numbering: – Type: volume Value: 32 – Type: issue Value: 3 Titles: – TitleFull: Philosophy & Technology Type: main |
| ResultId | 1 |
