Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Thomas Lamiaux, Matthieu Sozeau, Nicolas Tabareau, Yannick Forster
DOI: 10.5281/zenodo.19643714
Cited by: 1

Abstract

Source code for the implementation accompanying the paper titled "Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq".

Fields of Study & Subjects

Quality and Supply Management Business Strategies and Innovation Competitive and Knowledge Intelligence

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
18 April 2026