Search results

certicoq.org, certicoq.github.io

Status: Open.

#140 In CertiRocq/certirocq;

· andrew-appel opened on Mar 12, 2026

Targeting haskell ?

Status: Open.

#128 In CertiRocq/certirocq;

· spitters opened on Nov 28, 2025

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

Status: Open.

#121 In CertiRocq/certirocq;

· zoep opened on Jan 29, 2025

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

Status: Open.

#120 In CertiRocq/certirocq;

· mattam82 opened on Jan 28, 2025

CertiCoq to Misra-C

Status: Open.

#119 In CertiRocq/certirocq;

· mattam82 opened on Jan 28, 2025

Finish Beginning-to-End theorem

Status: Open.

#118 In CertiRocq/certirocq;

· mattam82 opened on Jan 28, 2025

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

Status: Open.

#117 In CertiRocq/certirocq;

· mattam82 opened on Jan 28, 2025

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

Status: Open.

#116 In CertiRocq/certirocq;

· mattam82 opened on Jan 28, 2025

Benchmark suite

Status: Open.

#114 In CertiRocq/certirocq;

· zoep opened on Jan 28, 2025

Uncurry transformation and proof

Status: Open.

#113 In CertiRocq/certirocq;

· zoep opened on Jan 27, 2025

Finish LambdaANF Correctness Proof

Status: Open.

#111 In CertiRocq/certirocq;

· mattam82 opened on Jan 27, 2025

32 bit version of CertiCoq

Status: Open.

#110 In CertiRocq/certirocq;

· mattam82 opened on Jan 27, 2025