Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2018.1
URN: urn:nbn:de:0030-drops-114052
URL: https://drops.dagstuhl.de/opus/volltexte/2019/11405/
Berger, Ulrich ; Matthes, Ralph ; Setzer, Anton
Martin Hofmann's Case for Non-Strictly Positive Data Types
| pdf-format: |
|
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 first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. 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.
BibTeX - Entry
@InProceedings{berger_et_al:LIPIcs:2019:11405,
author = {Ulrich Berger and Ralph Matthes and Anton Setzer},
title = {{Martin Hofmann's Case for Non-Strictly Positive Data Types}},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
pages = {1:1--1:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-106-1},
ISSN = {1868-8969},
year = {2019},
volume = {130},
editor = {Peter Dybjer and Jos{\'e} Esp{\'\i}rito Santo and Lu{\'\i}s Pinto},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11405},
URN = {urn:nbn:de:0030-drops-114052},
doi = {10.4230/LIPIcs.TYPES.2018.1},
annote = {Keywords: non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haske}
}
| Keywords: | non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haske | |
| Seminar: | 24th International Conference on Types for Proofs and Programs (TYPES 2018) | |
| Issue date: | 2019 | |
| Date of publication: | 18.11.2019 | |
| Supplementary Material: | https://github.com/rmatthes/breadthfirstalahofmann |
