Skip to content

Latest commit

 

History

History

array

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