All Projects → GeoCoq → Geocoq

GeoCoq / Geocoq

Licence: lgpl-3.0
A formalization of geometry in Coq based on Tarski's axiom system

Projects that are alternatives of or similar to Geocoq

Algorithms
A collection of algorithms and data structures
Stars: ✭ 11,553 (+8925.78%)
Mutual labels:  geometry
Ceramist
Verified hash-based AMQ structures in Coq
Stars: ✭ 107 (-16.41%)
Mutual labels:  coq
Aardvark.base
Aardvark is an open-source platform for visual computing, real-time graphics and visualization. This repository is the basis for most platform libraries and provides basic functionality such as data-structures, math and much more.
Stars: ✭ 117 (-8.59%)
Mutual labels:  geometry
Coq Pipes
Stars: ✭ 101 (-21.09%)
Mutual labels:  coq
Polylidar
Polylidar3D - Fast polygon extraction from 3D Data
Stars: ✭ 106 (-17.19%)
Mutual labels:  geometry
Coqtail
Interactive Coq Proofs in Vim
Stars: ✭ 109 (-14.84%)
Mutual labels:  coq
S2geometry
Computational geometry and spatial indexing on the sphere
Stars: ✭ 1,339 (+946.09%)
Mutual labels:  geometry
Svg.skia
An SVG rendering library.
Stars: ✭ 122 (-4.69%)
Mutual labels:  geometry
Lazysets.jl
A Julia package for calculus with convex sets
Stars: ✭ 107 (-16.41%)
Mutual labels:  geometry
Wagyu
A general library for geometry operations of union, intersections, difference, and xor
Stars: ✭ 116 (-9.37%)
Mutual labels:  geometry
Root
The official repository for ROOT: analyzing, storing and visualizing big data, scientifically
Stars: ✭ 1,377 (+975.78%)
Mutual labels:  geometry
Mindless Coding
Mindless, verified (erasably) coding using dependent types
Stars: ✭ 104 (-18.75%)
Mutual labels:  coq
Awesome Provable
A curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-13.28%)
Mutual labels:  coq
Peacoq
PeaCoq is a pretty Coq, isn't it?
Stars: ✭ 99 (-22.66%)
Mutual labels:  coq
Coq Of Ocaml
Import OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-8.59%)
Mutual labels:  coq
Hgeometry
HGeometry
Stars: ✭ 98 (-23.44%)
Mutual labels:  geometry
Ergo
The Language for Smart Legal Contracts
Stars: ✭ 108 (-15.62%)
Mutual labels:  coq
Tigl
The TiGL Geometry Library to process aircraft geometries in pre-design.
Stars: ✭ 123 (-3.91%)
Mutual labels:  geometry
Fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-7.03%)
Mutual labels:  coq
Iron
Coq formalizations of functional languages.
Stars: ✭ 114 (-10.94%)
Mutual labels:  coq

GeoCoq

A formalization of geometry in Coq.

This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.

Details and installation instructions can be found here: http://geocoq.github.io/GeoCoq/

Bug reports: https://github.com/GeoCoq/GeoCoq/issues

Mailing list: https://groups.google.com/forum/?hl=fr#!forum/geocoq

Build Status

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].