Analysis of the Coq Proof Management System

This repository contains the research work with respect to the core principles of the Coq Proof Management System as part of project work (team of 3) for CS 550 (Programming Languages and Theory) at Drexel Univeristy 2016.

Repository Structure

The Repository contains the following:

• The Project report (cs550_e_group3_Report.pdf) - An overall summary report of the research we conducted in this project. We recommend a reading of this report before looking at content in all other folders
• part1 - Presentation & Code (Proofs) for Simple Imperative Programs using Principles of IMP.
• part2 - Presentation & code (Proofs) for Small Step Operational Semantics and its importance towards Parallel Computation.
• part3 - Presentation for Simply Typed Lambda Calculus and demonstrations of its Principles using proofs in Coq (Code).

Dependencies

To run the code we recommend to download the Coq IDE available from the website, https://coq.inria.fr/