Conference Paper/Proceeding/Abstract 894 views 100 downloads
Martin Hofmann’s case for non-strictly positive data types
Leibniz International Proceedings in Informatics, LIPIcs, Volume: 130, Issue: 1
Swansea University Authors:
Ulrich Berger , Anton Setzer
-
PDF | Version of Record
Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).
Download (616.53KB)
DOI (Published version): 10.4230/LIPIcs.TYPES.2018.1
Abstract
We describe the breadth-first traversal algorithm by Martin Hofmann that usesa non-strictly positive data type and carry out a simple verification in anextensional setting. Termination is shown by implementing the algorithm inthe strongly normalising extension of system F by Mendler-style recursion....
Published in: | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
ISBN: | 978-395977106-1 |
ISSN: | 18688969 |
Published: |
2019
|
Online Access: |
Check full text
|
URI: | https://cronfa.swan.ac.uk/Record/cronfa51924 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
first_indexed |
2019-09-17T04:17:52Z |
---|---|
last_indexed |
2020-06-26T19:03:25Z |
id |
cronfa51924 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2020-06-26T15:50:48.1612810</datestamp><bib-version>v2</bib-version><id>51924</id><entry>2019-09-16</entry><title>Martin Hofmann’s case for non-strictly positive data types</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</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>2019-09-16</date><deptcode>SCS</deptcode><abstract>We describe the breadth-first traversal algorithm by Martin Hofmann that usesa non-strictly positive data type and carry out a simple verification in anextensional setting. Termination is shown by implementing the algorithm inthe strongly normalising extension of system F by Mendler-style recursion.We then analyze the same algorithm by alternative verifications in anintensional setting, in a setting with non-strictly positive inductivedefinitions (not just non-strictly positive data types), and one by algebraicreduction. The verification approaches are compared in terms of notions ofsimulation and should elucidate the somewhat mysterious algorithm and thusmake a case for other uses of non-strictly positive data types. Except forthe termination proof, which cannot be formalised in Coq, all proofs wereformalised in Coq and some of the algorithms were implemented in Agda andHaskell.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Leibniz International Proceedings in Informatics, LIPIcs</journal><volume>130</volume><journalNumber>1</journalNumber><publisher/><isbnElectronic>978-395977106-1</isbnElectronic><issnElectronic>18688969</issnElectronic><keywords>non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell</keywords><publishedDay>19</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2019</publishedYear><publishedDate>2019-11-19</publishedDate><doi>10.4230/LIPIcs.TYPES.2018.1</doi><url>https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11405</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2020-06-26T15:50:48.1612810</lastEdited><Created>2019-09-16T22:09:41.9412040</Created><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Ralph</firstname><surname>Matthes</surname><order>2</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>3</order></author></authors><documents><document><filename>0051924-16092019221537.pdf</filename><originalFilename>finalSubmission.pdf</originalFilename><uploaded>2019-09-16T22:15:37.2000000</uploaded><type>Output</type><contentLength>572908</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807> |
spelling |
2020-06-26T15:50:48.1612810 v2 51924 2019-09-16 Martin Hofmann’s case for non-strictly positive data types 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2019-09-16 SCS We describe the breadth-first traversal algorithm by Martin Hofmann that usesa non-strictly positive data type and carry out a simple verification in anextensional setting. Termination is shown by implementing the algorithm inthe strongly normalising extension of system F by Mendler-style recursion.We then analyze the same algorithm by alternative verifications in anintensional setting, in a setting with non-strictly positive inductivedefinitions (not just non-strictly positive data types), and one by algebraicreduction. The verification approaches are compared in terms of notions ofsimulation and should elucidate the somewhat mysterious algorithm and thusmake a case for other uses of non-strictly positive data types. Except forthe termination proof, which cannot be formalised in Coq, all proofs wereformalised in Coq and some of the algorithms were implemented in Agda andHaskell. Conference Paper/Proceeding/Abstract Leibniz International Proceedings in Informatics, LIPIcs 130 1 978-395977106-1 18688969 non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell 19 11 2019 2019-11-19 10.4230/LIPIcs.TYPES.2018.1 https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11405 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2020-06-26T15:50:48.1612810 2019-09-16T22:09:41.9412040 Ulrich Berger 0000-0002-7677-3582 1 Ralph Matthes 2 Anton Setzer 0000-0001-5322-6060 3 0051924-16092019221537.pdf finalSubmission.pdf 2019-09-16T22:15:37.2000000 Output 572908 application/pdf Version of Record true Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY). true eng |
title |
Martin Hofmann’s case for non-strictly positive data types |
spellingShingle |
Martin Hofmann’s case for non-strictly positive data types Ulrich Berger Anton Setzer |
title_short |
Martin Hofmann’s case for non-strictly positive data types |
title_full |
Martin Hofmann’s case for non-strictly positive data types |
title_fullStr |
Martin Hofmann’s case for non-strictly positive data types |
title_full_unstemmed |
Martin Hofmann’s case for non-strictly positive data types |
title_sort |
Martin Hofmann’s case for non-strictly positive data types |
author_id_str_mv |
61199ae25042a5e629c5398c4a40a4f5 5f7695285397f46d121207120247c2ae |
author_id_fullname_str_mv |
61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger 5f7695285397f46d121207120247c2ae_***_Anton Setzer |
author |
Ulrich Berger Anton Setzer |
author2 |
Ulrich Berger Ralph Matthes Anton Setzer |
format |
Conference Paper/Proceeding/Abstract |
container_title |
Leibniz International Proceedings in Informatics, LIPIcs |
container_volume |
130 |
container_issue |
1 |
publishDate |
2019 |
institution |
Swansea University |
isbn |
978-395977106-1 |
issn |
18688969 |
doi_str_mv |
10.4230/LIPIcs.TYPES.2018.1 |
url |
https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11405 |
document_store_str |
1 |
active_str |
0 |
description |
We describe the breadth-first traversal algorithm by Martin Hofmann that usesa non-strictly positive data type and carry out a simple verification in anextensional setting. Termination is shown by implementing the algorithm inthe strongly normalising extension of system F by Mendler-style recursion.We then analyze the same algorithm by alternative verifications in anintensional setting, in a setting with non-strictly positive inductivedefinitions (not just non-strictly positive data types), and one by algebraicreduction. The verification approaches are compared in terms of notions ofsimulation and should elucidate the somewhat mysterious algorithm and thusmake a case for other uses of non-strictly positive data types. Except forthe termination proof, which cannot be formalised in Coq, all proofs wereformalised in Coq and some of the algorithms were implemented in Agda andHaskell. |
published_date |
2019-11-19T04:03:59Z |
_version_ |
1763753317875318784 |
score |
11.021648 |