Skip to content

Issues: CertiCoq/certicoq

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

18 Open 10 Closed
18 Open 10 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Proposal: Introduce a Low-Level Intermediate Representation (LLIR) for CertiCoq
#121 opened Jan 29, 2025 by zoep
Move certicoqchk (CertiCoq-compiled MetaCoq checker) to its own repo
#120 opened Jan 28, 2025 by mattam82
CertiCoq to Misra-C
#119 opened Jan 28, 2025 by mattam82
Finish Beginning-to-End theorem
#118 opened Jan 28, 2025 by mattam82
1
LambdaBoxMut.compile no longer needs to use a view / wf-recursion
#117 opened Jan 28, 2025 by mattam82
Cleanup LambdaBoxMut/compile.v to disallow Var/Evar/...
#116 opened Jan 28, 2025 by mattam82
Benchmark suite
#114 opened Jan 28, 2025 by zoep
@zoep @yforster
1
Uncurry transformation and proof
#113 opened Jan 27, 2025 by zoep
Finish LambdaANF Correctness Proof
#111 opened Jan 27, 2025 by mattam82
@zoep
1
32 bit version of CertiCoq
#110 opened Jan 27, 2025 by mattam82
Remove the LambdaBoxMut language, translating directly from LambdaBox to LambdaBoxLocal
#109 opened Jan 27, 2025 by mattam82
3 tasks
4
Build instructions are out of date
#107 opened Jan 14, 2025 by zoep
1
Build instructions fail
#104 opened Nov 27, 2024 by nikos-alexandris
opam version compatible with Coq 8.17?
#102 opened Oct 16, 2024 by JasonGross
We should test with gcc and compcert's ccomp
#91 opened Feb 9, 2024 by mattam82
correctness proof of Codegen doesn't compile
#64 opened Apr 19, 2023 by womeier
3
CertiCoq FFI produces bad C code
#56 opened Aug 20, 2022 by kuruczgy
5
Support for efficient primitives
#24 opened Sep 30, 2020 by annenkov
13
ProTip! Follow long discussions with comments:>50.