Pinned Repositories
aoc-2022
CPP_Lib
Collection of C++ algorithms
FunctionalEditor
An editor for functional programming languages (WIP).
Lam
A formally verified interpreter for Lambda Calculus.
lean-smt
lean-syntax-highlight
A plugin for Obsidian that provides syntax highlight for Lean.
Reconstruction
RunTimeFormalization
A formalization of the run time complexity of Insertion Sort and Merge Sort.
RuntimeFormalization4
Porting https://github.com/tomaz1502/RunTimeFormalization to Lean 4
TinySAT
A tiny proof producing SAT solver.
tomaz1502's Repositories
tomaz1502/lean-syntax-highlight
A plugin for Obsidian that provides syntax highlight for Lean.
tomaz1502/RunTimeFormalization
A formalization of the run time complexity of Insertion Sort and Merge Sort.
tomaz1502/Lam
A formally verified interpreter for Lambda Calculus.
tomaz1502/RuntimeFormalization4
Porting https://github.com/tomaz1502/RunTimeFormalization to Lean 4
tomaz1502/dotfiles
Making setups easier
tomaz1502/TinySAT
A tiny proof producing SAT solver.
tomaz1502/lean-smt
tomaz1502/master-thesis
tomaz1502/signatures
Proof signatures for CVC4
tomaz1502/babeld
The Babel routing daemon
tomaz1502/Biblioteca
Biblioteca de algoritmos, estruturas de dados e primitivas para Maratona de Programação da UFMG.
tomaz1502/c_unit
Unit Tests in C
tomaz1502/CompCert
The CompCert formally-verified C compiler
tomaz1502/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
tomaz1502/cvc5
CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
tomaz1502/desert
tomaz1502/ffi_smt
tomaz1502/foo
tomaz1502/masters-defense
tomaz1502/mathlib4
The math library of Lean 4
tomaz1502/metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
tomaz1502/obsidian-releases
Community plugins list, theme list, and releases of Obsidian.
tomaz1502/opam
Archive for all Coq related OPAM packages organized in various repositories
tomaz1502/prism
Lightweight, robust, elegant syntax highlighting.
tomaz1502/process_lean_smt
tomaz1502/rinha-de-algoritmos
Na Rinha de Algoritmos você deve utilizar suas habilidades para a criação de algoritmos eficientes para resolver problemas!
tomaz1502/smtcoq
Communication between Coq and SAT/SMT solvers
tomaz1502/smtcoq-ci
Files for SMTCoq CI
tomaz1502/sniper
tomaz1502/tmux-battery
Plug and play battery percentage and icon indicator for Tmux.