No Cover Image

Conference Paper/Proceeding/Abstract 696 views 52 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
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
College: Faculty of Science and Engineering
Start Page: 1:1
End Page: 1:22

Similar Items