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

DOI10.4230/LIPIcs.TYPES.2018.1OpenAlexW2991146782MaRDI QIDQ5091141

Ralph Matthes, Anton Setzer, Ulrich Berger

Publication date: 21 July 2022

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

zbMATH Keywords

theorem provingprogram verificationCoqsystem Fbreadth-first traversalagdahaskemendler-style recursionnon strictly-positive data types

Mathematics Subject Classification ID

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

Related Items (1)

Temporal refinements for guarded recursive types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Parametricity and variants of Girard's \(J\) operator
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• Breadth-first numbering
• Computer Science Logic

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