Exploring Concepts of Interactive Theorem Proving

This paper formally presents the Calculus of Inductive Constructions (CiC), the expressive type system behind the Coq proof assistant. We begin with a brief review of the untyped λ-calculus and progressively build the CiC framework. As a case study, we formalize in Coq the proof that is a natural number for all , and relate it to its traditional counterpart. We then extract the Coq proof to Haskell, illustrating the Curry-Howard Isomorphism. The paper also examines the role of dependent types and heterogeneous equality, discusses the controlled use of axioms in dependently typed proofs, and outlines strategies for avoiding axioms to simplify reasoning.