Loading…
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the...
Saved in:
| Published in: | Logical methods in computer science 2024-01, Vol.20, Issue 1 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | English |
| Subjects: | |
| Online Access: | Get full text |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| cited_by | |
|---|---|
| cites | |
| container_end_page | |
| container_issue | |
| container_start_page | |
| container_title | Logical methods in computer science |
| container_volume | 20, Issue 1 |
| creator | Powell, Thomas |
| description | We introduce an extension of first-order logic that comes equipped with
additional predicates for reasoning about an abstract state. Sequents in the
logic comprise a main formula together with pre- and postconditions in the
style of Hoare logic, and the axioms and rules of the logic ensure that the
assertions about the state compose in the correct way. The main result of the
paper is a realizability interpretation of our logic that extracts programs
into a mixed functional/imperative language. All programs expressible in this
language act on the state in a sequential manner, and we make this intuition
precise by interpreting them in a semantic metatheory using the state monad.
Our basic framework is very general, and our intention is that it can be
instantiated and extended in a variety of different ways. We outline in detail
one such extension: A monadic version of Heyting arithmetic with a wellfounded
while rule, and conclude by outlining several other directions for future work. |
| doi_str_mv | 10.46298/lmcs-20(1:7)2024 |
| format | article |
| fullrecord | <record><control><sourceid>doaj_cross</sourceid><recordid>TN_cdi_doaj_primary_oai_doaj_org_article_883d297d31ad42f1abb743ca6aac2b82</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><doaj_id>oai_doaj_org_article_883d297d31ad42f1abb743ca6aac2b82</doaj_id><sourcerecordid>oai_doaj_org_article_883d297d31ad42f1abb743ca6aac2b82</sourcerecordid><originalsourceid>FETCH-LOGICAL-c306t-30e2517e0f6aec74e7e150912ac81080cca15098f6eb3775cb33b41baecb003c3</originalsourceid><addsrcrecordid>eNpNkU9LAzEQxRdRULQfwFuOCq7mz3aT9lZErSDoQc9hkp1dU7bNMomKJ7-62yriwDDzHsMPhlcUp4JfVrWcmat-7VMp-ZmY63PJZbVXHAlT83I609X-v_2wmKS04mMpJYysj4qvJ4qxTQwSSxkytm89Gyh2BOs0ZwvWBkq5jNQgsT52wbOPkF8ZuJQJfGbLCIQsUxh6TBcMNs3YLGwy0kA4EkPcybiz1wPSaL0j62HTvUGHJ8VBC33Cye88Ll5ub56vl-XD49399eKh9IrXuVQc5VRo5G0N6HWFGsWUz4QEbwQ33HvYatPW6JTWU--UcpVw47Ebn_XquLj_4TYRVnagsAb6tBGC3RmROguUg-_RGqMaOdONEtBUshXgnK6UhxrAS2fkyBI_LE8xJcL2jye43QVit4FYya2w2m4DUd-iMYHJ</addsrcrecordid><sourcetype>Open Website</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language</title><source>EZB Electronic Journals Library</source><creator>Powell, Thomas</creator><creatorcontrib>Powell, Thomas</creatorcontrib><description>We introduce an extension of first-order logic that comes equipped with
additional predicates for reasoning about an abstract state. Sequents in the
logic comprise a main formula together with pre- and postconditions in the
style of Hoare logic, and the axioms and rules of the logic ensure that the
assertions about the state compose in the correct way. The main result of the
paper is a realizability interpretation of our logic that extracts programs
into a mixed functional/imperative language. All programs expressible in this
language act on the state in a sequential manner, and we make this intuition
precise by interpreting them in a semantic metatheory using the state monad.
Our basic framework is very general, and our intention is that it can be
instantiated and extended in a variety of different ways. We outline in detail
one such extension: A monadic version of Heyting arithmetic with a wellfounded
while rule, and conclude by outlining several other directions for future work.</description><identifier>ISSN: 1860-5974</identifier><identifier>EISSN: 1860-5974</identifier><identifier>DOI: 10.46298/lmcs-20(1:7)2024</identifier><language>eng</language><publisher>Logical Methods in Computer Science e.V</publisher><subject>computer science - logic in computer science ; mathematics - logic</subject><ispartof>Logical methods in computer science, 2024-01, Vol.20, Issue 1</ispartof><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Powell, Thomas</creatorcontrib><title>Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language</title><title>Logical methods in computer science</title><description>We introduce an extension of first-order logic that comes equipped with
additional predicates for reasoning about an abstract state. Sequents in the
logic comprise a main formula together with pre- and postconditions in the
style of Hoare logic, and the axioms and rules of the logic ensure that the
assertions about the state compose in the correct way. The main result of the
paper is a realizability interpretation of our logic that extracts programs
into a mixed functional/imperative language. All programs expressible in this
language act on the state in a sequential manner, and we make this intuition
precise by interpreting them in a semantic metatheory using the state monad.
Our basic framework is very general, and our intention is that it can be
instantiated and extended in a variety of different ways. We outline in detail
one such extension: A monadic version of Heyting arithmetic with a wellfounded
while rule, and conclude by outlining several other directions for future work.</description><subject>computer science - logic in computer science</subject><subject>mathematics - logic</subject><issn>1860-5974</issn><issn>1860-5974</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2024</creationdate><recordtype>article</recordtype><sourceid>DOA</sourceid><recordid>eNpNkU9LAzEQxRdRULQfwFuOCq7mz3aT9lZErSDoQc9hkp1dU7bNMomKJ7-62yriwDDzHsMPhlcUp4JfVrWcmat-7VMp-ZmY63PJZbVXHAlT83I609X-v_2wmKS04mMpJYysj4qvJ4qxTQwSSxkytm89Gyh2BOs0ZwvWBkq5jNQgsT52wbOPkF8ZuJQJfGbLCIQsUxh6TBcMNs3YLGwy0kA4EkPcybiz1wPSaL0j62HTvUGHJ8VBC33Cye88Ll5ub56vl-XD49399eKh9IrXuVQc5VRo5G0N6HWFGsWUz4QEbwQ33HvYatPW6JTWU--UcpVw47Ebn_XquLj_4TYRVnagsAb6tBGC3RmROguUg-_RGqMaOdONEtBUshXgnK6UhxrAS2fkyBI_LE8xJcL2jye43QVit4FYya2w2m4DUd-iMYHJ</recordid><startdate>20240101</startdate><enddate>20240101</enddate><creator>Powell, Thomas</creator><general>Logical Methods in Computer Science e.V</general><scope>AAYXX</scope><scope>CITATION</scope><scope>DOA</scope></search><sort><creationdate>20240101</creationdate><title>Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language</title><author>Powell, Thomas</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c306t-30e2517e0f6aec74e7e150912ac81080cca15098f6eb3775cb33b41baecb003c3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2024</creationdate><topic>computer science - logic in computer science</topic><topic>mathematics - logic</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Powell, Thomas</creatorcontrib><collection>CrossRef</collection><collection>Directory of Open Access Journals</collection><jtitle>Logical methods in computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Powell, Thomas</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language</atitle><jtitle>Logical methods in computer science</jtitle><date>2024-01-01</date><risdate>2024</risdate><volume>20, Issue 1</volume><issn>1860-5974</issn><eissn>1860-5974</eissn><abstract>We introduce an extension of first-order logic that comes equipped with
additional predicates for reasoning about an abstract state. Sequents in the
logic comprise a main formula together with pre- and postconditions in the
style of Hoare logic, and the axioms and rules of the logic ensure that the
assertions about the state compose in the correct way. The main result of the
paper is a realizability interpretation of our logic that extracts programs
into a mixed functional/imperative language. All programs expressible in this
language act on the state in a sequential manner, and we make this intuition
precise by interpreting them in a semantic metatheory using the state monad.
Our basic framework is very general, and our intention is that it can be
instantiated and extended in a variety of different ways. We outline in detail
one such extension: A monadic version of Heyting arithmetic with a wellfounded
while rule, and conclude by outlining several other directions for future work.</abstract><pub>Logical Methods in Computer Science e.V</pub><doi>10.46298/lmcs-20(1:7)2024</doi><oa>free_for_read</oa></addata></record> |
| fulltext | fulltext |
| identifier | ISSN: 1860-5974 |
| ispartof | Logical methods in computer science, 2024-01, Vol.20, Issue 1 |
| issn | 1860-5974 1860-5974 |
| language | eng |
| recordid | cdi_doaj_primary_oai_doaj_org_article_883d297d31ad42f1abb743ca6aac2b82 |
| source | EZB Electronic Journals Library |
| subjects | computer science - logic in computer science mathematics - logic |
| title | Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-28T15%3A34%3A10IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-doaj_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Proofs%20as%20stateful%20programs:%20A%20first-order%20logic%20with%20abstract%20Hoare%20triples,%20and%20an%20interpretation%20into%20an%20imperative%20language&rft.jtitle=Logical%20methods%20in%20computer%20science&rft.au=Powell,%20Thomas&rft.date=2024-01-01&rft.volume=20,%20Issue%201&rft.issn=1860-5974&rft.eissn=1860-5974&rft_id=info:doi/10.46298/lmcs-20(1:7)2024&rft_dat=%3Cdoaj_cross%3Eoai_doaj_org_article_883d297d31ad42f1abb743ca6aac2b82%3C/doaj_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c306t-30e2517e0f6aec74e7e150912ac81080cca15098f6eb3775cb33b41baecb003c3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true |