volodeyka

I do formal verification with interactive theorem provers

National University of SingaporeSingapore

Pinned Repositories

coq-lgtm
Framework for Hyper-safety proofs about structured data
Language:Coq3 3 11
lean-ssr
LeanSSR: an SSReflect-Like Tactic Language for Lean
Language:Lean32 1 180
splean
Separation Logic Proofs in Lean
Language:Lean283
compilers-2020
Language:TeX0 0 00
coqspec
Verified Specifier of S-Graph Language
Language:Coq3 1 00
csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
Language:HTML0 0 00
CT2021
Language:TeX0 0 00
Danan
Language:OCaml0 2 20
okasaki
Coq library to deal with purely functional data structures
Language:Coq3 5 00
trust-coq
Formalization of the Truly Stateless Concurrency Model Checker in Coq
Language:Coq13 1 00

volodeyka's Repositories

volodeyka/trust-coq
Formalization of the Truly Stateless Concurrency Model Checker in Coq
Language:Coq13 1 00
volodeyka/coqspec
Verified Specifier of S-Graph Language
Language:Coq3 1 00
volodeyka/okasaki
Coq library to deal with purely functional data structures
Language:Coq3 5 00
volodeyka/compilers-2020
Language:TeX0 0 00
volodeyka/csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
Language:HTML0 0 00
volodeyka/CT2021
Language:TeX0 0 00
volodeyka/Danan
Language:OCaml0 2 20
volodeyka/DT2021-1
0 0 00
volodeyka/finmap
Finite sets, finite maps, multisets and generic sets
Language:Coq0 0 00
volodeyka/loogle
Mathlib search tool
Language:Lean0 0
volodeyka/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Language:JavaScript0 0
volodeyka/veri-sparse
Language:Dafny3 0
volodeyka/volodeyka.github.io
Language:HTML1 0