From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 51805BC69 for ; Wed, 11 Apr 2007 15:15:15 +0200 (CEST) Received: from mailironport.loria.fr (mailironport.loria.fr [152.81.144.100]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l3BDFEum000419 for ; Wed, 11 Apr 2007 15:15:15 +0200 Received: from chicoree.loria.fr ([152.81.11.82]) by mailironport.loria.fr with ESMTP; 11 Apr 2007 15:16:03 +0200 X-IronPort-AV: i="4.14,395,1170630000"; d="scan'208"; a="11900498:sNHT25965772" Received: by chicoree.loria.fr (Postfix, from userid 1709) id E7D5810078; Wed, 11 Apr 2007 15:15:12 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by chicoree.loria.fr (Postfix) with ESMTP id E749A10077 for ; Wed, 11 Apr 2007 15:15:12 +0200 (CEST) Date: Wed, 11 Apr 2007 15:15:12 +0200 (CEST) From: Frederic Blanqui To: caml-list@yquem.inria.fr Subject: INRIA PhD position In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Miltered: at concorde with ID 461CDF62.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; invariants:01 subset:01 invariants:01 ocaml:01 rewriting:01 2007.:98 abstract:01 functions:01 functions:01 data:02 data:02 defined:02 theorem:02 structures:02 structures:02 Title: Generation of construction functions guaranteeing algebraic invariants on concrete data types Aim: Although concrete data types are very useful in defining complex data structures, they are not always sufficient to adequately specify the data structures required by some algorithms. Often, only a subset of the concrete data type is in fact used since some invariants between the components are mandatory to ensure the correctness of the program. Now, many invariants can be described by using some equational theory. For instance, a sorted list is a particular representative of the equivalence class of lists modulo commutativity. The usual way to solve this problem is to use abstract data types or, better, private data types if one does not want to lose the ability of doing pattern matching. We propose to study the automatic generation of certified construction functions guaranteeing algebraic invariants on concrete data types, and develop an extension of OCaml with relational data types, that is, data types with invariants described by user defined equations. More information and online application on: http://www.talentsplace.com/syndication1/inria/frdoc/details.html?id=PGTFK02620$ Competences and pro The position involves research and development in the area of functional programming, rewriting theory (in particular Knuth-Bendix completion) and interactive theorem proving. Speaking french is not necessary. Salary: the monthly gross salary is approx. EUR 1,875. Environment: - laboratory: LORIA (http://www.loria.fr/) - team: Protheo (http://protheo.loria.fr/) - project: Quotient (http://quotient.loria.fr/) - location: Nancy, in the East of France is at 1:30 from Paris by tren, 1:30 from Luxembourg airport by car, and 1:30 from Germany and Belgium. Application deadline: 30 April 2007. Contact: Frederic Blanqui (http://www.loria.fr/~blanqui/) More information about INRIA PhD positions: http://www.inria.fr/travailler/opportunites/doc.en.html