No Cover Image

Conference Paper/Proceeding/Abstract 785 views 79 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
Tags: Add Tag
No Tags, Be the first to tag this record!
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

Similar Items