CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions

DOI10.1007/11916277_18zbMath1165.03322OpenAlexW1845410252WikidataQ62042540 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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

Size-based termination of higher-order rewriting ⋮ Mixed Inductive/Coinductive Types and Strong Normalization ⋮ Is sized typing for Coq practical? ⋮ Unnamed Item ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ A compact kernel for the calculus of inductive constructions

This page was built for publication: CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions