Extracting Purely Functional Contents from Logical Inductive Types

We propose a method to extract purely functional contents from logical inductive types in the context of the Calculus of Inductive Constructions. This method is based on a mode consistency analysis, which veries if a computation is possible w.r.t. the selected inputs/outputs, and the code generation itself. We prove that this extraction is sound w.r.t. the Calculus of Inductive Constructions. Finally, we present some optimizations, as well as the implementation designed in the Coq proof assistant framework.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: David Delahaye, Catherine Dubois, Jean-Frédéric Étienne
• Keywords: Artificial Intelligence, Inductive Constructions, Logical Inductive Types, Mode Consistency Analysis, TPHOL 2007