Name: Patrick Nicodemus
Type: User
Company: University of Pennsylvania
Bio: Computational biology in Python and R.
Formally verified mathematics in Coq.
Twitter: PatNicodemus
Location: Philadelphia, Pennsylvania
Blog: math.wisc.edu/~nicodemus
Patrick Nicodemus's Projects
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
A Python package using Gromov-Wasserstein distance to compare cell shapes
An axiom-free formalization of category theory in Coq for personal study and practical work
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.
Git repository containing the Futhark website.
A port of CAJAL to OCaml.
Homotopy type theory
Context sensitive completion for OCaml in Vim and Emacs
Network Analysis in Python
An OCaml kernel for Jupyter (IPython) notebook
Owl - OCaml Scientific Computing @ http://ocaml.xyz
Website repository.
A foundational framework for modular cryptographic proofs in Coq
Python library for loading and using triangular meshes.
Owl Tutorial
Implementation of the Gromov-Wasserstein distance to the setting of Unbalanced Optimal Transport
Main website for MMT and related material
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.