Estou iniciando meus estudos em computação teórica e formalização matemática de programas. Este estudo servirá como base para compreender melhor paradigmas de programação, compiladores e verificação de sistemas críticos.
Embora ROCQ (antigo Coq) seja o foco principal, o estudo não se limitará apenas a essa ferramenta. Programação funcional, linguagens formais, autômatos, cálculo lambda e outros assuntos relacionados à essência da ciência da computação também serão abordados posteriormente neste repositório.
Nos últimos meses em que estive ativo no GitHub, compartilhei projetos pessoais, trabalhos de disciplinas da faculdade e projetos desenvolvidos para a FnEsc, entre outros.
Abaixo estão alguns dos principais repositórios que servirão como base para a construção deste repositório:
- Aprendendo o paradigma funcional com Haskell
- Aprendendo sobre a máquina de Turing com um simulador online
- Experimento com cálculo diferencial e integral aplicado com Haskell
- Meu simulador da placa Apple Juice em C++ com Raylib
.
├── LICENSE
├── README.md
├── para-curiosos # Compartilho sobre o assunto sem me aprofundar
│ └── helloworld.v
└── src
├── formal-language-theory # Aqui ficam meus estudos sobre linguagens formais
│ └── Notas de Aula.pdf
├── lambda-calculus # Aqui ficam meus estudos sobre lambda calculus
│ └── introduction.pdf
└── rocq # Aqui ficam meus estudos sobre Rocq Proof
├── 01-fundamentos
│ ├── a_tipos.v
│ └── b_definicoes.v
├── 02-funcoes
└── a_recursao.v
├── 03-provas
├── 04-estruturas_dados
└── 05-tipos_dependentes
Rocq não permite que nomes de arquivos comecem com números ou contenham hífens.
Para evitar problemas, utilizarei a ordem alfabética na organização dos arquivos e adotarei esse padrão em todo o repositório.