GeezerVison is showing github.com — GitHub - gabritto/Coq-CSP: Coq definitions and proofs for a tiny subset of CSP (communicating sequential processes)

Open more actions menu

Latest commit

History

45 Commits

Folders and files

Name		Name	Last commit message	Last commit date
project		project
.gitignore		.gitignore
README.md		README.md
aula02_gallina.v		aula02_gallina.v
aula03_provas.v		aula03_provas.v
aula04_inducao.v		aula04_inducao.v
aula05_listas.v		aula05_listas.v
aula06_poli.v		aula06_poli.v
aula07_alta_ordem.v		aula07_alta_ordem.v
aula08_taticas.v		aula08_taticas.v
aula09_logica.v		aula09_logica.v
aula10_negb_n_times.v		aula10_negb_n_times.v
aula11_prop_indutivas.v		aula11_prop_indutivas.v
aula12_auto.v		aula12_auto.v
makefile		makefile
negb_n_times.v		negb_n_times.v

Repository files navigation

Coq-CSP

Code for the Advanced Topics in Software Engineering (TAES) course. The course used Coq to develop programs and prove properties about them. There are Coq files for each class, with completed exercises. There is also a project that defines a tiny subset of CSP, a traces semantic for it, and proves the correctness of the functional definition of traces with regards to the inductive relation definition of traces.

About

Coq definitions and proofs for a tiny subset of CSP (communicating sequential processes)

Resources

Readme

Activity

Stars

0 stars

Watchers

1 watching

Forks

1 fork

Report repository

GeezerVison