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.
-
Notifications
You must be signed in to change notification settings - Fork 1
gabritto/TAES
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Coq definitions and proofs for a tiny subset of CSP (communicating sequential processes)
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published