All Projects → coq-io → Hello World

coq-io / Hello World

Licence: mit
A Hello World program in Coq.

Labels

Projects that are alternatives of or similar to Hello World

Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+4757.14%)
Mutual labels:  coq
Cpp2v
Formalization of C++ for verification purposes.
Stars: ✭ 24 (+71.43%)
Mutual labels:  coq
Dblib Linear
Formalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-28.57%)
Mutual labels:  coq
Software Foundations
Coq proofs of exercises in Pierce's book
Stars: ✭ 5 (-64.29%)
Mutual labels:  coq
Micro Policies Coq
Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (+28.57%)
Mutual labels:  coq
Cufp 2015 Tutorial
An introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-35.71%)
Mutual labels:  coq
Sf Zh
《软件基础》中译版 Software Foundations Chinese Translation
Stars: ✭ 554 (+3857.14%)
Mutual labels:  coq
Ledgertheory
Stars: ✭ 12 (-14.29%)
Mutual labels:  coq
Autosubst
Automation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (+57.14%)
Mutual labels:  coq
Software Foundations
Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-35.71%)
Mutual labels:  coq
Crimp
Certified Relational to Imperative
Stars: ✭ 5 (-64.29%)
Mutual labels:  coq
Coq Guarded Computational Type Theory
Stars: ✭ 18 (+28.57%)
Mutual labels:  coq
Hott Species
Combinatorial species in HoTT
Stars: ✭ 9 (-35.71%)
Mutual labels:  coq
Pudding
KCoFI Pudding: The formal proofs for the KCoFI system
Stars: ✭ 5 (-64.29%)
Mutual labels:  coq
Coqjvm
Coq executable semantics and resource verifier
Stars: ✭ 10 (-28.57%)
Mutual labels:  coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+3914.29%)
Mutual labels:  coq
Coqpie
CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)
Stars: ✭ 8 (-42.86%)
Mutual labels:  coq
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (+0%)
Mutual labels:  coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+6100%)
Mutual labels:  coq
Monads
Coq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-35.71%)
Mutual labels:  coq

Logo Hello World

A Hello World program in Coq.

build status

Install from opam

Make sure you added the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-io-hello-world
helloWorld

Install from source

Compile the Coq code:

./configure.sh
make

Compile and execute the generated OCaml:

cd extraction/
make
./main.native
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].