Home

Welcome to the PL-Project wiki! This is the course project for the CS263 Programming Language, which formalizes the asymptotic time complexity for a toy language, proposes and proves the soundness of several useful Hoare rules.

Project Overview

Our project has the following files:

• Imp9.v: basic library of the toy language, from the course.
• PolyAB.v: defines polynomial and its operation, asymptotic bounds defined on polynomials, and some lemmas.
• Denotation.v: defines the denotational semantics with steps, mainly from the course but modified.
• HoareLogic.v: defines the Hoare logic with asymptotic bound and Hoare rules.
• Soundness.v: the proof for the soundness of Hoare rules in HoareLogic.v.
• Demos.v: examples of correctness and time complexity of programs proved using our Hoare rules.

Compilation Order

To be able to run the code, please compile the project in the following order:

• Imp9.v -> PolyAB.v -> Denotation.v -> HoareLogic.v -> Soundness.v -> Demos.v