Applications of Coq Formal proofs of mathematical theorems Formal proof of 4-color theorem By Georges Gonthier and Benjamin Werner,2004 Other:Feit-Thompson theorem proved in Coq in 2012 ·Formal verification OS kernels and hypervisors CertiKOS project at Yale seL4 in Isabelle at NICTA ·Compilers CompCert at INRIA and following projects LLVM verification and Upenn 。Others Web servers (bedrock projects MIT) Certified software tool chains(e.g.,analysis algorithms)@Princeton 。Teaching:logic,programming languages,…Applications of Coq • Formal proofs of mathematical theorems • Formal proof of 4-color theorem • By Georges Gonthier and Benjamin Werner, 2004 • Other: Feit–Thompson theorem proved in Coq in 2012 • Formal verification • OS kernels and hypervisors • CertiKOS project at Yale • seL4 in Isabelle at NICTA • Compilers • CompCert at INRIA and following projects • LLVM verification and Upenn • Others • Web servers (bedrock projects @ MIT) • Certified software tool chains (e.g., analysis algorithms) @ Princeton • Teaching: logic, programming languages, …