Final project for master's degree in Semantics of programming languages course.
-
Updated
Jun 22, 2025 - Haskell
#
Coq
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
Here are 9 public repositories matching this topic...
Run `coqc` and print out colorized Coq error location information
-
Updated
Oct 24, 2018 - Haskell
My master thesis (and related code) in Logic at the University of Bergen.
-
Updated
Feb 2, 2024 - Haskell
Implementation of EnvCap: A Programming Language with Capabilities as First-Class Modules using λₑ with extensions as the Core Calculus.
-
Updated
Oct 28, 2025 - Haskell
Decentralized blockchain-based storage of the automatically-verifiably correct (certified) code as well as generalized blockchain platform
-
Updated
Sep 23, 2017 - Haskell
🔪 OPG (Operator Precedence Grammar) Parser, in Coq.
-
Updated
Jun 25, 2021 - Haskell
Official repository of the Autosubst 2 project.
-
Updated
May 8, 2023 - Haskell
The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
-
Updated
Apr 24, 2020 - Haskell
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
- Followers
- 62 followers
- Repository
- coq/coq
- Website
- github.com/topics/coq
- Wikipedia
- Wikipedia