Skip to content

Latest commit

 

History

History
25 lines (20 loc) · 1002 Bytes

README.md

File metadata and controls

25 lines (20 loc) · 1002 Bytes
Raw

The correctness of the library Printer Сombinators with Сhoice

About

Here is the proof of the library correctness printer combinators with choice with Pareto filtering optimisation. The proof is relative to the base implementation.

Building the Project

Requirements

Building Manually

To build the project, one needs to install hahn library, which the project depends on. This might be done by running

opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive
opam install coq-hahn

After that, one needs to run make.

Description of code

  • FuncCorrect.v—correctness of combinators and layouts.
  • IsLess.v— partial order properties.
  • ListEqTrivalProof.v—relationship of the minimum height with the context lemma.
  • MinHeight.v— properties of the Pareto set and proof of the correctness of the library.