No Cover Image

Conference Paper/Proceeding/Abstract 152 views 6 downloads

Martin Hofmann’s case for non-strictly positive 1 data types / Ulrich, Berger

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

Swansea University Author: Ulrich, Berger

  • 50300.pdf

    PDF | Version of Record

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

    Download (571.29KB)

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
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Keywords: non strictly-positive data types, breadth-first traversal, program verifi30 cation, Mendler-style recursion, System F, theorem proving, Coq, Agda, Haskell
Start Page: 1:1
End Page: 1:22