Search results

Proposal: Introduce a Low-Level Intermediate Representation (LLIR) for CertiCoq

Status: Open.

#121 In CertiCoq/certicoq;

· zoep opened on Jan 29, 2025

Move certicoqchk (CertiCoq-compiled MetaCoq checker) to its own repo

Status: Open.

#120 In CertiCoq/certicoq;

· mattam82 opened on Jan 28, 2025

CertiCoq to Misra-C

Status: Open.

#119 In CertiCoq/certicoq;

· mattam82 opened on Jan 28, 2025

Finish Beginning-to-End theorem

Status: Open.

#118 In CertiCoq/certicoq;

· mattam82 opened on Jan 28, 2025

LambdaBoxMut.compile no longer needs to use a view / wf-recursion

Status: Open.

#117 In CertiCoq/certicoq;

· mattam82 opened on Jan 28, 2025

Cleanup LambdaBoxMut/compile.v to disallow Var/Evar/...

Status: Open.

#116 In CertiCoq/certicoq;

· mattam82 opened on Jan 28, 2025

Benchmark suite

Status: Open.

#114 In CertiCoq/certicoq;

· zoep opened on Jan 28, 2025

Uncurry transformation and proof

Status: Open.

#113 In CertiCoq/certicoq;

· zoep opened on Jan 27, 2025

Finish LambdaANF Correctness Proof

Status: Open.

#111 In CertiCoq/certicoq;

· mattam82 opened on Jan 27, 2025

32 bit version of CertiCoq

Status: Open.

#110 In CertiCoq/certicoq;

· mattam82 opened on Jan 27, 2025

Remove the LambdaBoxMut language, translating directly from LambdaBox to LambdaBoxLocal

Status: Open.

#109 In CertiCoq/certicoq;

· mattam82 opened on Jan 27, 2025

Build instructions are out of date

Status: Open.

#107 In CertiCoq/certicoq;

· zoep opened on Jan 14, 2025