Universality of proofs

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

Table of contents

Introduction 
1 Introduction 
1.1 Proof systems
1.1.1 Formalization of mathematics
1.1.2 Software verification
1.2 Universality of proofs
1.2.1 Computational reasoning
1.2.2 Higher-order reasoning
1.3 Type theory and logical frameworks
1.3.1 The Curry–Howard correspondence
1.3.2 The logical framework approach
1.4 Computational higher-order logics
1.4.1 Pure type systems
1.4.2 Universes and cumulativity
1.5 Contributions
1.6 Preliminary notions and notations
I Frameworks and embeddings 
2 The -calculus 
2.1 Definition
2.2 As a first-order logic calculus
2.3 As a logical framework
2.4 Limitations of
3 The -calculus modulo rewriting 
3.1 Definition
3.2 Basic properties
3.2.1 Soundness properties
3.2.2 Completeness properties
3.3 Computational higher-order embeddings
II Pure type systems 
4 Pure type systems 
4.1 Definition
4.2 Examples of pure type systems
4.3 Basic properties
4.4 Inter-system properties
4.4.1 Subsystems
4.4.2 Morphisms
5 Embedding pure type systems 
5.1 Translation
5.2 Completeness
5.2.1 Preservation of substitution
5.2.2 Preservation of equivalence
5.2.3 Preservation of typing
5.3 Alternative embeddings
5.3.1 Embedding without in the rewriting at the level of types
5.3.2 Embedding without rewriting at the level of types
6 Conservativity 
6.1 Normalization and conservativity
6.2 Proof of conservativity
6.2.1 Conservativity of equivalence
6.2.2 Conservativity of typing
7 Application: translating HOL to Dedukti 
7.1 HOL
7.2 Translation
7.2.1 Translation of types
7.2.2 Translation of terms
7.2.3 Translation of proofs
7.3 Completeness
7.4 Implementation
7.4.1 Proof retrieval
7.4.2 Holide: HOL to Dedukti
7.4.3 Extensions
III Cumulative and infinite hierarchies 
8 Cumulative type systems 
8.1 Definition
8.1.1 Specification and syntax
8.1.2 Subtyping
8.1.3 Typing
8.2 Basic properties
8.3 Inter-system properties
8.3.1 Subsystems
8.3.2 Morphisms
8.3.3 Closures
8.4 Principal typing
8.4.1 Definition
8.4.2 Derivation rules
8.4.3 Soundness
8.4.4 Completeness
8.5 Examples of CTSs with principal typing
9 Embedding cumulativity 
9.1 Translation
9.2 Completeness
9.2.1 Preservation of substitution
9.2.2 Preservation of equivalence
9.2.3 Preservation of typing
10 Infinite universe hierarchies 
10.1 Predicative universes
10.2 Impredicative universe
10.3 Cumulativity
11 Application: translating CIC to Dedukti 
11.1 Inductive types
11.1.1 Inductive types and eliminators
11.1.2 Eliminators in the -calculus modulo rewriting
11.2 Other features
11.2.1 Modules
11.2.2 Local let definitions and local fixpoints
11.2.3 Floating universes
11.2.4 Universe polymorphism
11.3 Implementation
11.3.1 Coqine: Coq to Dedukti
11.3.2 Krajono: Matita to Dedukti
Conclusion
12 Conclusion 
12.1 Related work
12.1.1 Logical embeddings
12.1.2 Proof interoperability
12.2 Future work
12.2.1 Improving the translations
12.2.2 Designing new embeddings
12.2.3 Interoperability in Dedukti
Appendix