[TYPES/announce] The 8th Coq Workshop - 2nd CFP - deadline for submission: june 1st 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Eighth Coq Workshop (2016) http://coq.inria.fr/coq-workshop/2016 <http://coq.inria.fr/coq-workshop/2016> Colocated with the 7th International Conference on Interactive Theorem Proving (ITP 2016) August 26, 2016 in Nancy, France The Coq Workshop series brings together Coq users, developers, and contributors. While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, likely supplemented with invited talks. Submission Instructions We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Relevant subject matter includes but is not limited to: * Language or tactic features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools and platforms built on Coq * Plugins and libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit short proposals through EasyChair. Submissions should be in portable document format (PDF). Proposals should not exceed 2 pages in length in single-column full-page style. Venue: Nancy, France Important Dates: * June 1: Deadline for proposal submission * June 15: Acceptance notification * August 26: Workshop in Nancy Submission URL: https://www.easychair.org/conferences/?conf=coq8 <https://www.easychair.org/conferences/?conf=coq8> Program committee: * Frédéric Blanqui, INRIA, France * Adam Chlipala, MIT, United States * Cyril Cohen, INRIA, France * Pierre Courtieu, CNAM, France * Jónathan Heras Vicente, University of La Rioja, Spain * Robbert Krebbers, Aarhus University, Denmark * Nicolas Magaud (co-chair), University of Strasbourg, France * Micaela Mayero, Univeristy of Paris 7, France * Julien Narboux (co-chair), University of Strasbourg, France * Claudio Sacerdoti-Coen, University of Bologna, Italy * Beta Ziliani, FAMAF, Universidad Nacional de Córdoba, Argentina, and CONICET, Argentina Organization: Contacts: Nicolas Magaud (mag...@unistra.fr <mailto:mag...@unistra.fr>), Julien Narboux (narb...@unistra.fr <mailto:narb...@unistra.fr>)
[TYPES/announce] PhD position available : Building reliable programs in computational geometry and certifying them with Coq
[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
A three-year PhD-student position is open at LSIIT
(http://lsiit.u-strasbg.fr )
in the field of formal proofs in geometry. This proposal fits in the
GALAPAGOS
research project which has been accepted by the french research agency
(ANR) in 2007.
This thesis will be supervised by Professor Jean-François Dufourd and
co-advised
by Nicolas Magaud (http://http://dpt-info.u-strasbg.fr/~jfd/ .
We would like it to start as soon as possible (at the end of 2007 at the
latest).
Context :
-
In the GALAPAGOS project, we wish to apply computerized theorem proving
tools to two aspects
of geometry. The first aspect concerns computational geometry, the
second step concerns verifying
geometric reasoning steps in usual constructions, such as constructions
with ruler and compass.
Thesis proposal : Building reliable programs in computational geometry
and certifying them
--
This thesis aims at improving software quality and at designing new
algorithms in the field
of computational geometry. To achieve this goal, we shall use
combinatorial maps as our
topological model and use formal methods to specify, interactively prove
and automatically
extract programs from their proofs of correctness.
This work will be carried out in the Calculus of Inductive Constructions
and implemented
via the Coq proof assistant. From a specification and a constructive
proof, its enables us
to extract an Ocaml program via the proofs-as-programs paradigm. This,
the program is
certified, meaning that it always terminates and that it satisfies its
specification.
Geometric objects we shall consider are plane subdivisions, modeled by
embedded combinatorial
maps. Embeddings will be linear and most combinatorial maps involved
will be planar.
This thesis will make us revisit classic problems in computational
geometry, among them,
handling plane subdivisions, computing convex hulls, performing point
location, co-refining
maps, computing Delaunay and Voronoï diagrams. This should be sufficient
to show our methodology
benefits, especially proof techniques for structural and/or noetherian
induction on subdivisions.
This will allow us to deal with more complex algorithms such as those
required in 3D.
Contact Information :
-
For further information about this position, please contact either:
Jean-François Dufourd [EMAIL PROTECTED]
Nicolas Magaud[EMAIL PROTECTED]
Applications should be directed to
{dufourd,[EMAIL PROTECTED] . Your application
should contain a resume and a cover letter as well as references (e.g.
your Master's thesis advisor).
--
Nicolas Magaudmailto:[EMAIL PROTECTED]
LSIIT - UMR 7005 CNRS-ULPTel: (+33) 3 90 24 45 61
Bd Sébastien Brant - BP 10413Fax: (+33) 3 90 24 44 55
67412 ILLKIRCH CEDEX - FRANCEhttp://dpt-info.u-strasbg.fr/~magaud
