Martin Hofmann's Case for Non-Strictly Positive Data Types - Assistance à la Certification d’Applications DIstribuées et Embarquées Accéder directement au contenu
Chapitre D'ouvrage Année : 2019

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

Résumé

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.
Fichier principal
Vignette du fichier
BergerMatthesSetzer-MartinHofmannsCase-TYPES2018-Postproc.pdf (571.29 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-02365814 , version 1 (15-11-2019)

Licence

Paternité

Identifiants

Citer

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⟩
277 Consultations
242 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More