coq_jupyter

Coq IDE kernel

A Jupyter notebook kernel for interactive theorem proving with Coq

Jupyter kernel for Coq

GitHub

94 stars
4 watching
7 forks
Language: Python
last commit: about 2 years ago
Linked from 2 awesome lists

coqdependent-typesjupyterjupyter-extensionjupyter-kernelsjupyter-notebookkernelproof-assistantpython-patheorem-proving

Backlinks from these awesome lists:

Related projects:

RepositoryDescriptionStars
ejgallego/pycoqPython bindings for Coq's interactive proof assistant50
ejgallego/coq-lspA tool for interactive theorem proving and language support in Coq153
princeton-vl/coqgymA learning environment for theorem proving with the Coq proof assistant388
ilyasergey/pnpA tutorial project on using Coq to mechanize mathematics with dependent types160
tani/acl2-kernelA Jupyter kernel extension that integrates ACL2 theorem proving into interactive computing environments.4
carglglz/jupyter_upydevice_kernelA Jupyter kernel for interacting with MicroPython boards over USB/Serial or WebREPL connections.14
robots-from-jupyter/robotkernelAn IPython kernel specifically designed for Robot Framework testing and execution in Jupyter Notebooks and Lab environments.75
tylere/ee-jupyter-examplesA collection of Jupyter Notebook examples showcasing the use of the Earth Engine Python API87
charguer/tlcA Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems.38
whonore/coqtailEnables interactive proof development in Vim similar to other proof assistants.274
formal-land/coq-of-pythonFormal verification of Python code using Coq30
xonsh/xontrib-jupyterA Jupyter kernel and notebook extension that integrates Xonsh shell into interactive computing environments.35
stisa/jupyternimA Jupyter kernel for the Nim programming language.164
plclub/lngenTool for generating Coq definitions and proofs for locally nameless representations30