[TYPES/announce] PhD position available : Building reliable programs in computational geometry and certifying them with Coq

[Nicolas Magaud]

[ 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

[TYPES/announce] Call for Participation - APLAS 2007

[Shengchao Qin]

[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


 
Call for Participation
  The Fifth Asian Symposium on Programming Languages and Systems
  November 29 - December 1, 2007
   Singapore
http://www.comp.nus.edu.sg/~aplas07/
http://flint.cs.yale.edu/aplas2007/
Scope of the Conference---
APLAS aims at stimulating programming language research by providing aforum for 
the presentation of recent results and the exchange of ideasand experience in 
topics concerned with programming languages andsystems.  APLAS is based in 
Asia, but is an international forum thatserves the worldwide programming 
languages community.
The APLAS series is sponsored by the Asian Association for Foundationof 
Software (AAFS), which has recently been founded by Asianresearchers in 
cooperation with many researchers from Europe and theUSA.  The past formal 
APLAS symposiums were successfully held inSydney (2006, Australia), Tsukuba 
(2005, Japan), Taipei (2004, Taiwan)and Beijing (2003, China) after three 
informal workshops held inShanghai (2002, China), Daejeon (2001, Korea) and 
Singapore (2000).Proceedings of the past symposiums were published in 
Springer-Verlag'sLNCS 2895, 3302, 3780, and 4279.
Conference Location---
APLAS'07 will be held at Kent Ridge Guild House, National Universityof 
Singapore.  Singapore is a dynamic city rich in contrast and colorwhere you'll 
find a harmonious blend of culture, cuisine, arts andarchitecture. A bridge 
between the East and the West for centuries,Singapore, located in the heart of 
fascinating Southeast Asia,continues to embrace tradition and modernity today. 
Brimming withunbridled energy and bursting with exciting events, the city 
offerscountless unique, memorable experiences waiting to be discovered.
Registration
The early registration deadline is set on 28Sept07. The registrationfees will 
cover conference proceeding, banquet dinner, andlunches/teas.
 Deadline  Full Fees  Student Feesearly28Sep07  
   S$600   S$400online   23Nov07 S$650   S$425
on-site  29Nov07 S$700   S$450
Payment can be made with credit cards. Exchange rate (subject tofluctuation) is 
approx. US$1 = S$1.53
Online registration can be made at:
 http://www.comp.nus.edu.sg/~aplas07/local.html#registration
Accommodation-
A special rate S$155 per nite (excluding taxes but inclusiveof daily breakfast) 
is applicable to attendees of APLAS 2007 atRendezvous Hotel Singapore:
http://www.rendezvoushotels.com/singapore/
The hotel is located in city center. A free daily shuttle bus will beprovided 
between this hotel and the conference site (at NUS) duringthe conference 
period.  Our block of rooms is guaranteed till28Sept07, so advanced booking is 
encouraged as some rooms may bereleased after this date. For reservation, 
please use a special formthat can be found at:
 http://www.comp.nus.edu.sg/~aplas07/Hotel.APLAS07.pdf
Poster Session--
APLAS07 will include a poster session. Submission deadlineis 14 Sept 2007. For 
details, please see:
 http://www.comp.nus.edu.sg/~aplas07/posters.html
Conference Program--
29 Nov (Thu)  915- 930 Opening note
  930-1030 Invited Talk
   X10: Programming Parallel Machines, Productively   Vijay 
Saraswat (IBM TJ Watson Research Lab)
1100-1230 Session 1
   The Nuggetizer: Abstracting Away Higher-Orderness   for 
Program Verification   Paritosh Shroff (Johns Hopkins University),  
 Christian Skalka (University of Vermont)   and Scott F. Smith 
(Johns Hopkins University)
   Local Reasoning for Storable Locks and Threads   Alexey 
Gotsman (University of Cambridge),   Josh Berdine (Microsoft Research), 
  Byron Cook (Microsoft Research),   Noam Rinetzky (Tel Aviv 
University)   and Mooly Sagiv (Tel Aviv University)
   Monadic, Prompt Lazy Assertions in Haskell   Frank Huch (CAU 
Kiel) and Olaf Chitil (University of Kent)
1345-1515 Session 2
   Translation Correctness for First-Order Object-Oriented   
Pattern Matching   Burak Emir (EPFL Lausanne), Qin Ma (OFFIS)   
and Martin Odersky (EPFL Lausanne)
   Persistent Oberon: A Programming Language with Integrated 
Persistence   Luc Blaser (ETH Zurich)
   More Typed Assembly Languages for Confidentiality   Dachuan 
Yu (DoCoMo Communication Laboratories USA)
1515-1630 Poster Session
1630-1730 Session 3
   A Novel Test Case Generation Method for Prolog Programs   
Based on Call Patterns Semantics   Lingzhong Zhao (Guilin University of 
Electronic Technology),   Tianlong Gu (Guilin