Designing and proving correct a convex hull algorithm with hypermaps in Coq (Q448980): Difference between revisions

@@ Property / Mathematics Subject Classification ID @@
+D18
@@ Property / Mathematics Subject Classification ID: 65D18 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+Y15
@@ Property / Mathematics Subject Classification ID: 65Y15 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6080929
@@ Property / zbMATH DE Number: 6080929 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+convex hull
@@ Property / zbMATH Keywords: convex hull / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+hypermaps
@@ Property / zbMATH Keywords: hypermaps / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+formal specifications
@@ Property / zbMATH Keywords: formal specifications / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+computer-aided proofs
@@ Property / zbMATH Keywords: computer-aided proofs / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Coq system
@@ Property / zbMATH Keywords: Coq system / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+computational geometry
@@ Property / zbMATH Keywords: computational geometry / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.comgeo.2010.06.006
+Normal rank
@@ Property / OpenAlex ID @@
+W2166210250
@@ Property / OpenAlex ID: W2166210250 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+A proof of GMP square root
@@ Property / cites work: A proof of GMP square root / rank @@
+Normal rank
@@ Property / cites work @@
+Q4217293
@@ Property / cites work: Q4217293 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4071773
@@ Property / cites work: Q4071773 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2747613
@@ Property / cites work: Q2747613 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5452284
@@ Property / cites work: Q5452284 / rank @@
+Normal rank
@@ Property / cites work @@
+Design and formal proof of a new optimal image segmentation program with hypermaps
+Normal rank
@@ Property / cites work @@
+Q4910724
@@ Property / cites work: Q4910724 / rank @@
+Normal rank
@@ Property / cites work @@
+Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
+Normal rank
@@ Property / cites work @@
+An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
+Normal rank
@@ Property / cites work @@
+Q3772828
@@ Property / cites work: Q3772828 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5302559
@@ Property / cites work: Q5302559 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075246
@@ Property / cites work: Q3075246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5615284
@@ Property / cites work: Q5615284 / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
+Normal rank
@@ Property / cites work @@
+Classroom examples of robustness problems in geometric computations
+Normal rank
@@ Property / cites work @@
+Axioms and hulls
@@ Property / cites work: Axioms and hulls / rank @@
+Normal rank
@@ Property / cites work @@
+Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
+Normal rank
@@ Property / cites work @@
+Automated Deduction in Geometry
@@ Property / cites work: Automated Deduction in Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790670
@@ Property / cites work: Q4790670 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3311639
@@ Property / cites work: Q3311639 / rank @@
+Normal rank
@@ Property / cites work @@
+Combinatorial Oriented Maps
@@ Property / cites work: Combinatorial Oriented Maps / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:448980