Skip to Main content Skip to Navigation
Book sections

Martin Hofmann's Case for Non-Strictly Positive Data Types

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.
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download
Contributor : Ralph Matthes <>
Submitted on : Friday, November 15, 2019 - 3:16:29 PM
Last modification on : Tuesday, September 8, 2020 - 9:22:02 AM
Long-term archiving on: : Sunday, February 16, 2020 - 6:06:12 PM


Publisher files allowed on an open archive


Distributed under a Creative Commons Attribution 4.0 International License



Ulrich Berger, Ralph Matthes, Anton Setzer. Martin Hofmann's Case for Non-Strictly Positive Data Types. Peter Dybjer; José Espírito Santo; Luís Pinto. 24th International Conference on Types for Proofs and Programs (TYPES 2018), 130, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.1:1-1:22, 2019, Leibniz International Proceedings in Informatics (LIPIcs), 978-3-95977-106-1. ⟨10.4230/LIPIcs.TYPES.2018.1⟩. ⟨hal-02365814⟩



Record views


Files downloads