Automated Proof Verification with Coq

About

This repository contains 2 coq files, and 2 corresponding write-ups. The coq files contain proofs of properties of 2-by-2 matrices, and properties of a simple Ocaml based language (including properties of its compilers, interpreters, and virtual machine). This repository is the result of Yale-NUS College's Function Programminga and Proving course (YSC3236) run in the fall of AY2017-18 by Professor Olivier Danvy.

The projects

The coq files for projects contain properties and theorems and their proofs. A detailed explanation of the theorems and properties in each coq file is provided in the write-up corresponding to the file.

Running the coq files

[TODO]

Author

Oishik Ganguly

Acknowledgements

Thanks to Professor Olivier Danvy.