No Cover Image

Conference Paper/Proceeding/Abstract 154 views 14 downloads

Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda

Harry Bryant, Andrew Lawrence, Monika Seisenberger Orcid Logo, Anton Setzer Orcid Logo

Types 2025, Pages: 186 - 189

Swansea University Authors: Harry Bryant, Monika Seisenberger Orcid Logo, Anton Setzer Orcid Logo

  • abstractBryantTypes2025.pdf

    PDF | Accepted Manuscript

    Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).

    Download (117.76KB)
Published in: Types 2025
Published: Glasgow, UK 2025
Online Access: https://msp.cis.strath.ac.uk/types2025/TYPES2025-book-of-abstracts.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa70913
first_indexed 2025-11-16T13:52:13Z
last_indexed 2026-01-16T05:32:42Z
id cronfa70913
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2026-01-15T12:38:21.7204595</datestamp><bib-version>v2</bib-version><id>70913</id><entry>2025-11-16</entry><title>Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda</title><swanseaauthors><author><sid>2efb4f6a3eec27ae4337ecd971aaeca4</sid><firstname>Harry</firstname><surname>Bryant</surname><name>Harry Bryant</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-11-16</date><deptcode>MACS</deptcode><abstract/><type>Conference Paper/Proceeding/Abstract</type><journal>Types 2025</journal><volume/><journalNumber/><paginationStart>186</paginationStart><paginationEnd>189</paginationEnd><publisher/><placeOfPublication>Glasgow, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>9</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2025</publishedYear><publishedDate>2025-06-09</publishedDate><doi/><url>https://msp.cis.strath.ac.uk/types2025/TYPES2025-book-of-abstracts.pdf</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2026-01-15T12:38:21.7204595</lastEdited><Created>2025-11-16T13:26:19.3029380</Created><path><level id="1"/><level id="2"/></path><authors><author><firstname>Harry</firstname><surname>Bryant</surname><order>1</order></author><author><firstname>Andrew</firstname><surname>Lawrence</surname><order>2</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>3</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>4</order></author></authors><documents><document><filename>70913__35640__78db721e1ece4ca5a20314ba8c79e022.pdf</filename><originalFilename>abstractBryantTypes2025.pdf</originalFilename><uploaded>2025-11-16T13:45:09.5778107</uploaded><type>Output</type><contentLength>120585</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><documentNotes>Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/deed.en</licence></document></documents><OutputDurs/></rfc1807>
spelling 2026-01-15T12:38:21.7204595 v2 70913 2025-11-16 Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda 2efb4f6a3eec27ae4337ecd971aaeca4 Harry Bryant Harry Bryant true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2025-11-16 MACS Conference Paper/Proceeding/Abstract Types 2025 186 189 Glasgow, UK 9 6 2025 2025-06-09 https://msp.cis.strath.ac.uk/types2025/TYPES2025-book-of-abstracts.pdf COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2026-01-15T12:38:21.7204595 2025-11-16T13:26:19.3029380 Harry Bryant 1 Andrew Lawrence 2 Monika Seisenberger 0000-0002-2226-386X 3 Anton Setzer 0000-0001-5322-6060 4 70913__35640__78db721e1ece4ca5a20314ba8c79e022.pdf abstractBryantTypes2025.pdf 2025-11-16T13:45:09.5778107 Output 120585 application/pdf Accepted Manuscript true Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention). true eng https://creativecommons.org/licenses/by/4.0/deed.en
title Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
spellingShingle Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
Harry Bryant
Monika Seisenberger
Anton Setzer
title_short Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
title_full Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
title_fullStr Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
title_full_unstemmed Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
title_sort Verifying Z3 RUPproofs with the interactive theorem provers Coq/Rocq and Agda
author_id_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4
d035399b2b324a63fe472ce0344653e0
5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4_***_Harry Bryant
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Harry Bryant
Monika Seisenberger
Anton Setzer
author2 Harry Bryant
Andrew Lawrence
Monika Seisenberger
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title Types 2025
container_start_page 186
publishDate 2025
institution Swansea University
url https://msp.cis.strath.ac.uk/types2025/TYPES2025-book-of-abstracts.pdf
document_store_str 1
active_str 0
published_date 2025-06-09T05:33:56Z
_version_ 1856987030230138880
score 11.096212

Similar Items