- Lambda Calculos and Type theory too
- Examples of such tools include SAT solvers, SMT solvers, and model checkers.
- JavaCard platform
- highest level of common criteria certification
- Specifications of the X86
- LLVM instruction sets (or only LLVM)
- I will put a part of the book text to be better to read xD.
As an environment for developing formally certified software and hardware, Coq has been used, for example, to build CompCert, a fully-verified optimizing compiler for C, and CertiKOS, a fully verified hypervisor, for proving the correctness of subtle algorithms involving floating point numbers, and as the basis for CertiCrypt, an environment for reasoning about the security of cryptographic algorithms. It is also being used to build verified implementations of the open-source RISC-V processor architecture
- Feit-Thompson Theorem
- Calculus of Constructions
- Map reduce
The most basic tenet of functional programming is that, as much as possible, computation should be pure, in the sense that the only effect of execution should be to produce a result: it should be free from side effects such as I/O, assignments to mutable variables, redirecting pointers, etc. For example, whereas an imperative sorting function might take a list of numbers and rearrange its pointers to put the list in order, a pure sorting function would take the original list and return a new list containing the same numbers in sorted order