Skip to content

Latest commit

 

History

History
26 lines (18 loc) · 894 Bytes

README.md

File metadata and controls

26 lines (18 loc) · 894 Bytes

Improving the LRAT checker with arrays (manually)

compilation: An LRAT checker built on CakeML with arrays

lpr_arrayFullProgScript.sml: This builds the cake_lpr proof checker

lpr_arrayPackingProgScript.sml: This builds a proof checker specialized to the packing chromatic number bounds

lpr_arrayParsingProgScript.sml: Adds a parser for LPR

lpr_arrayProgScript.sml: This refines lpr_list to use arrays

lpr_arrayRamseyProgScript.sml: This builds a proof checker specialized to Ramsey number 4

lpr_composeProgScript.sml: Define and verify LPR composition checker function

lpr_listScript.sml: This refines the LPR checker to a fixed-size, list-based implementation