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

DOI10.4230/LIPICS.TYPES.2018.1MaRDI QIDQ5091141zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Ralph Matthes, Anton Setzer

Publication date 21 July 2022

Full work available at URL https://hal.archives-ouvertes.fr/hal-02365814

zbMATH Keywords

agdabreadth-first traversalCoqhaskemendler-style recursionnon strictly-positive data typesprogram verificationsystem Ftheorem proving

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Containers: Constructing strictly positive types
• Certification of breadth-first algorithms by extraction
• Termination of algorithms over non-freely generated data types
• Foundational nonuniform (co)datatypes for higher-order logic
• Positive inductive-recursive definitions

Cites work

• Breadth-first numbering
• Computer Science Logic
• scientific article; zbMATH DE number 3882404 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• Parametricity and variants of Girard's \(J\) operator
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types

Cited in

(2)

• Temporal refinements for guarded recursive types
• Infinitary refinement types for temporal properties in Scott domains

This page was built for publication: Martin Hofmann's Case for Non-Strictly Positive Data Types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5091141)