Conference Paper/Proceeding/Abstract 973 views 112 downloads
Martin Hofmann’s case for non-strictly positive data types
,
Ralph Matthes,
Anton Setzer
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 |
| 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. |
|---|---|
| Keywords: |
non strictly-positive data types, breadth-first traversal, program verification, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell |
| Issue: |
1 |