No Cover Image

Conference Paper/Proceeding/Abstract 826 views 78 downloads

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

Ulrich Berger Orcid Logo, Ralph Matthes, Anton Setzer

24th International Conference on Types for Proofs and Programs, Volume: 130, Pages: 1:1 - 1:22

Swansea University Author: Ulrich Berger Orcid Logo

  • 50300.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution License CC-BY (CC-BY).

    Download (571.29KB)

Check full text

DOI (Published version): 10.4230/LIPIcs.TYPES.2018.1

Abstract

We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursi...

Full description

Published in: 24th International Conference on Types for Proofs and Programs
ISBN: 978-3-95977-106-1
ISSN: 1868-8969
Published: Dagstuhl, Germany 2019
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa50300
first_indexed 2019-05-13T10:26:30Z
last_indexed 2023-02-22T03:58:01Z
id cronfa50300
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2023-02-21T16:15:19.6553320</datestamp><bib-version>v2</bib-version><id>50300</id><entry>2019-05-09</entry><title>Martin Hofmann&#x2019;s case for non-strictly positive 1 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></swanseaauthors><date>2019-05-09</date><deptcode>MACS</deptcode><abstract>We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications in an intensional setting, in a setting with non-strictly positive inductive definitions (not just non-strictly positive data types), and one by algebraic reduction. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>24th International Conference on Types for Proofs and Programs</journal><volume>130</volume><journalNumber/><paginationStart>1:1</paginationStart><paginationEnd>1:22</paginationEnd><publisher/><placeOfPublication>Dagstuhl, Germany</placeOfPublication><isbnPrint/><isbnElectronic>978-3-95977-106-1</isbnElectronic><issnPrint/><issnElectronic>1868-8969</issnElectronic><keywords>non strictly-positive data types, breadth-first traversal, program verifi30 cation, 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>http://drops.dagstuhl.de/opus/volltexte/2019/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/><funders/><projectreference/><lastEdited>2023-02-21T16:15:19.6553320</lastEdited><Created>2019-05-09T22:38:42.0348985</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><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><order>3</order></author></authors><documents><document><filename>50300__16661__c3674961fe4d490ba27ddcab5be67b74.pdf</filename><originalFilename>50300.pdf</originalFilename><uploaded>2020-02-21T13:00:01.3730100</uploaded><type>Output</type><contentLength>584996</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Released under the terms of a Creative Commons Attribution License CC-BY (CC-BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2023-02-21T16:15:19.6553320 v2 50300 2019-05-09 Martin Hofmann’s case for non-strictly positive 1 data types 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2019-05-09 MACS We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications in an intensional setting, in a setting with non-strictly positive inductive definitions (not just non-strictly positive data types), and one by algebraic reduction. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell. Conference Paper/Proceeding/Abstract 24th International Conference on Types for Proofs and Programs 130 1:1 1:22 Dagstuhl, Germany 978-3-95977-106-1 1868-8969 non strictly-positive data types, breadth-first traversal, program verifi30 cation, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell 19 11 2019 2019-11-19 10.4230/LIPIcs.TYPES.2018.1 http://drops.dagstuhl.de/opus/volltexte/2019/11405/ COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2023-02-21T16:15:19.6553320 2019-05-09T22:38:42.0348985 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Ralph Matthes 2 Anton Setzer 3 50300__16661__c3674961fe4d490ba27ddcab5be67b74.pdf 50300.pdf 2020-02-21T13:00:01.3730100 Output 584996 application/pdf Version of Record true Released under the terms of a Creative Commons Attribution License CC-BY (CC-BY). true https://creativecommons.org/licenses/by/4.0/
title Martin Hofmann’s case for non-strictly positive 1 data types
spellingShingle Martin Hofmann’s case for non-strictly positive 1 data types
Ulrich Berger
title_short Martin Hofmann’s case for non-strictly positive 1 data types
title_full Martin Hofmann’s case for non-strictly positive 1 data types
title_fullStr Martin Hofmann’s case for non-strictly positive 1 data types
title_full_unstemmed Martin Hofmann’s case for non-strictly positive 1 data types
title_sort Martin Hofmann’s case for non-strictly positive 1 data types
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Ralph Matthes
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title 24th International Conference on Types for Proofs and Programs
container_volume 130
container_start_page 1:1
publishDate 2019
institution Swansea University
isbn 978-3-95977-106-1
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.TYPES.2018.1
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://drops.dagstuhl.de/opus/volltexte/2019/11405/
document_store_str 1
active_str 0
description We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications in an intensional setting, in a setting with non-strictly positive inductive definitions (not just non-strictly positive data types), and one by algebraic reduction. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.
published_date 2019-11-19T07:44:34Z
_version_ 1821390641339301888
score 11.047891

Similar Items