Coq development for Kernel computations

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

Table of contents

0 Introduction 
0.1 Effective homology
0.2 Coq
0.3 Conventions & notations
0.4 Premises
I Mathematics to compute 
1 A theory of sets 
1.1 Bishopian toolkit
1.2 Categories
1.3 Choice!
2 Homological algebra in type theory 
2.1 Homology
2.2 Abelian categories will not fit
2.3 Preabelian categories
2.4 Graded objects and chain complexes
2.5 Kernels of matrices
II Intermezzo: Down to Coq Implementation 
3 Efficient computations 
3.1 A brief history of N
3.2 Going native
3.3 Performance
3.4 Related works
4 A new tactic engine 
4.1 Refinement
4.2 Combining tactics
4.3 About the implementation
4.4 Further work
III Faster, Higher, Stronger 
5 On the category of sets 
5.1 Topoi
5.2 Quasitopoi
5.3 Internal language
6 Sharing more code 
6.1 Categories & additive categories
6.2 Sets as categories and beyond
6.3 The category of graded objects is preabelian
Appendices
A Coq development for Kernel computations
A.1 Kernels are finite dimensional
A.2 Testing the program
B Strong subsets are classified
Conclusion 
Bibliography