No Cover Image

Conference Paper/Proceeding/Abstract 973 views 112 downloads

Martin Hofmann’s case for non-strictly positive data types

Ulrich Berger Orcid Logo, Ralph Matthes, Anton Setzer Orcid Logo

Leibniz International Proceedings in Informatics, LIPIcs, Volume: 130, Issue: 1

Swansea University Authors: Ulrich Berger Orcid Logo, Anton Setzer Orcid Logo

  • finalSubmission.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).

    Download (616.53KB)

Check full text

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....

Full description

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
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&#x2019;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>MACS</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>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</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 MACS 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 Mathematics and Computer Science School COLLEGE CODE MACS 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-19T07:48:17Z
_version_ 1821390875326939136
score 11.047804

Similar Items