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: 3 months ago
Linked from 2 awesome lists

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

Backlinks from these awesome lists:

Related projects:

Repository Description Stars
ejgallego/pycoq Python bindings for Coq's interactive proof assistant 50
ejgallego/coq-lsp A tool for interactive theorem proving and language support in Coq 152
princeton-vl/coqgym A learning environment for theorem proving with the Coq proof assistant 384
ilyasergey/pnp A tutorial project on using Coq to mechanize mathematics with dependent types 160
tani/acl2-kernel A Jupyter kernel extension that integrates ACL2 theorem proving into interactive computing environments. 4
carglglz/jupyter_upydevice_kernel A Jupyter kernel for interacting with MicroPython boards over USB/Serial or WebREPL connections. 14
robots-from-jupyter/robotkernel An IPython kernel specifically designed for Robot Framework testing and execution in Jupyter Notebooks and Lab environments. 75
tylere/ee-jupyter-examples A collection of Jupyter Notebook examples showcasing the use of the Earth Engine Python API 87
charguer/tlc A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. 38
whonore/coqtail Enables interactive proof development in Vim similar to other proof assistants. 274
formal-land/coq-of-python Formal verification of Python code using Coq 30
xonsh/xontrib-jupyter A Jupyter kernel and notebook extension that integrates Xonsh shell into interactive computing environments. 35
stisa/jupyternim A Jupyter kernel for the Nim programming language. 163
plclub/lngen Tool for generating Coq definitions and proofs for locally nameless representations 30