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

DOI10.1007/11916277_18MaRDI QIDQ5387897zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Gilles Barthe, Benjamin Grégoire, Fernando Pastawski

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)

Recommendations

• Linear sized types in the calculus of constructions
• On strong normalization of the calculus of constructions with type-based termination
• A Tutorial on Type-Based Termination
• Type-Based Termination with Sized Products
• Semi-continuous Sized Types and Termination

Cited in

(19)

• A compact kernel for the calculus of inductive constructions
• A predicative analysis of structural recursion
• Mixed Inductive/Coinductive Types and Strong Normalization
• Type-Based Termination with Sized Products
• scientific article; zbMATH DE number 2061698 (Why is no real title available?)
• Type-based termination of recursive definitions
• Size-based termination of higher-order rewriting
• Termination checking with types
• On strong normalization of the calculus of constructions with type-based termination
• Linear sized types in the calculus of constructions
• A Tutorial on Type-Based Termination
• Computer Science Logic
• Typed Lambda Calculi and Applications
• Partiality and recursion in interactive theorem provers -- an overview
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Semi-continuous Sized Types and Termination
• Is sized typing for Coq practical?
• Type-based termination of generic programs

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

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