Jean-François Dufourd

Theor. Comput. Sci., 2015

2014

Formal specification and proofs for the topology and classification of combinatorial surfaces.

[BibT_eX]

[DOI]

Comput. Geom., 2014

Hypermap Specification and Certified Linked Implementation Using Orbits.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2014

2012

Designing and proving correct a convex hull algorithm with hypermaps in Coq.

[BibT_eX]

[DOI]

Christophe Brun

Nicolas Magaud

Comput. Geom., 2012

Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls.

[BibT_eX]

[DOI]

Christophe Brun

Nicolas Magaud

Proceedings of the Automated Deduction in Geometry - 9th International Workshop, 2012

2010

Edge Collision Detection in Complex Deformable Environments.

[BibT_eX]

[DOI]

Thomas Jund

Proceedings of the Seventh Workshop on Virtual Reality Interactions and Physical Simulations, 2010

Formal Study of Plane Delaunay Triangulation.

[BibT_eX]

[DOI]

Yves Bertot

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps.

[BibT_eX]

[DOI]

J. Autom. Reason., 2009

Particle-based forecast mechanism for continuous collision detection in deformable environments.

[BibT_eX]

[DOI]

Thomas Jund

Proceedings of the 2009 ACM Symposium on Solid and Physical Modeling, 2009

2008

Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2008

Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps.

[BibT_eX]

[DOI]

Proceedings of the STACS 2008, 2008

2007

Design and formal proof of a new optimal image segmentation program with hypermaps.

[BibT_eX]

[DOI]

Pattern Recognit., 2007

A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler's formula.

[BibT_eX]

[DOI]

Proceedings of the 2007 ACM Symposium on Applied Computing (SAC), 2007

2004

Formalizing the trading theorem in Coq.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2004

Formalizing generalized maps in Coq.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2004

2003

Combination of Automatic and Interactive Tools for Solution Space Browsing.

[BibT_eX]

[DOI]

Caroline Essert-Villard

Pascal Mathis

Proceedings of the 2003 International Conference on Geometric Modeling and Graphics, 2003

2002

Formalizing the Trading Theorem for the Classification of Surfaces.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Interacting with parametrized geometric objects using lambda-terms.

[BibT_eX]

[DOI]

Sven Luther

Proceedings of the Seventh ACM Symposium on Solid Modeling and Applications, 2002

Parametrizing geometric objects using λ-calculus.

[BibT_eX]

[DOI]

Sven Luther

Proceedings of the 18th Spring Conference on Computer Graphics, 2002

2000

Formalizing mathematics in higher-order logic: A case study in geometric modelling.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2000

Functional specification and prototyping with oriented combinatorial maps.

[BibT_eX]

[DOI]

Comput. Geom., 2000

Sketch-based pruning of a solution space within a formal geometric constraint solver.

[BibT_eX]

[DOI]

Caroline Essert-Villard

Artif. Intell., 2000

Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Geometry, Third International Workshop, 2000

1999

A formal specification of geometric refinements.

[BibT_eX]

[DOI]

Vis. Comput., 1999

1998

Geometric Construction by Assembling Solved Subfigures.

[BibT_eX]

[DOI]

Pascal Mathis

Artif. Intell., 1998

Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Formal Program Development in Geometric Modeling.

[BibT_eX]

[DOI]

Proceedings of the Applied Formal Methods, 1998

1997

Algebras and formal specifications in geometric modelling.

[BibT_eX]

[DOI]

Vis. Comput., 1997

Formal Resolution of Geometrical Constraint Systems by Assembling.

[BibT_eX]

[DOI]

Pascal Mathis

Proceedings of the Fourth Symposium on Solid Modeling and Applications, 1997

Term Rewrite Systems to Derive Set Boolean Operations on 2D Objects.

[BibT_eX]

[DOI]

Proceedings of the FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 1997

1994

Algebraic Specification of a 3D-Modeler Based on Hypermaps.

[BibT_eX]

[DOI]

Yves Bertrand

CVGIP Graph. Model. Image Process., 1994

1993

Algebraic Specification and Development in Geometric Modeling.

[BibT_eX]

[DOI]

Yves Bertrand

Jean Françon

Pascal Lienhardt

Proceedings of the TAPSOFT'93: Theory and Practice of Software Development, 1993

1991

Formal specification of topological subdivisions using hypermaps.

[BibT_eX]

[DOI]

Comput. Aided Des., 1991

An OBJ3 functional specification for boundary representation.

[BibT_eX]

[DOI]

Proceedings of the first ACM Symposium on Solid Modeling Foundations and CAD/CAM Applications, 1991

1989

A Topological Map-Based Kernel for Polyhedron Modelers: Algebraic Specification and Logic Prototyping.

[BibT_eX]

[DOI]

Proceedings of the 10th European Computer Graphics Conference and Exhibition, 1989

1988

Construction of Interactive Programs in Computer Graphics.

[BibT_eX]

[DOI]