The Calculus of Inductive Constructions

For more info about our services contact : help@bestpfe.com

Table of contents

1 Introduction 
1.1 A brief history of type theory
1.2 Safety of Proof assistants
1.3 Contributions
1.4 Outline of the thesis
2 The Calculus of Presburger Inductive Constructions 
2.1 Terms of the calculus
2.2 The conversion relation
2.3 Two simple examples
2.4 Typing rules
2.5 Consistency
3 The Calculus of Congruent Inductive Constructions 
3.1 The Calculus of Inductive Constructions
3.2 Parametric multi-sorted theories with constructors
3.3 The calculus
4 Meta-theoretical Properties of CCIC 
4.1 Conuence on well-sorted terms
4.2 Monotony of conversion
4.3 Weakening
4.4 Substitutivity
4.5 Product compatibility
4.6 Correctness of types
4.7 Subject reduction
4.8 Type unicity
4.9 Strong normalization
5 Deciding CCIC 
5.1 Decidability of conversion relation
5.2 A syntax oriented typing judgment
5.3 Deciding more theories
6 Conclusion and perspectives 
6.1 Stability of extractable equations
6.2 Using a typed extraction
6.3 Weak terms
6.4 Extending CCIC to CAC
6.5 Embedding a more powerful logic
Bibliography