CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
From MaRDI portal
Publication:5387897
DOI10.1007/11916277_18zbMath1165.03322WikidataQ62042540 ScholiaQ62042540MaRDI QIDQ5387897
Benjamin Grégoire, Fernando Pastawski, Gilles Barthe
Publication date: 27 May 2008
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11916277_18
Related Items
Size-based termination of higher-order rewriting, Unnamed Item, Partiality and recursion in interactive theorem provers – an overview, Is sized typing for Coq practical?, A compact kernel for the calculus of inductive constructions, Mixed Inductive/Coinductive Types and Strong Normalization