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.7 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id AF33CBBC1 for ; Mon, 3 Mar 2008 08:31:31 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAAI4y0dC+VLvg2dsb2JhbACQcAEBAQgEBBMYkgiIKA X-IronPort-AV: E=Sophos;i="4.25,436,1199660400"; d="scan'208";a="23279924" Received: from wx-out-0506.google.com ([66.249.82.239]) by mail4-smtp-sop.national.inria.fr with ESMTP; 03 Mar 2008 08:31:31 +0100 Received: by wx-out-0506.google.com with SMTP id h27so5582157wxd.15 for ; Sun, 02 Mar 2008 23:31:30 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; bh=bX5b5Y0JgfyTjPlco0EnHVJUu9bVvaKHZ1N9WCZM9BY=; b=Pp3ap8unS+U1msqaG1Z83EHO9DaxXqJQYd8ilErNSlfV8HWdh3mj4njC0oeJcx5SaLQf6JnmHfuDbKgS5r0ulQIXOfkpCdcPpZg1eeB47YVqaQ1mt4sr1xDvVEbpkVhpc0DkkNsboVRi7IpK2qZCqbEOMRcEqc0T3zHca4WN+go= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=N3wmo/M1wBgNq8u9gz2vnKQLPR2QwKBMq+g2qRG4mfHFv5LUdJ0x2BcnKuBz/g0oKdoSVBpQjDwKBo8wYNq6Pur08WutDzer+5pQ2TGDUr8dJDAUBYzeOdsBBv1Bj5ZgxIsoZn5grDy86r7mUAhj//NBloxjDY1yMkHxTbNRvxI= Received: by 10.70.47.19 with SMTP id u19mr11950263wxu.1.1204529489904; Sun, 02 Mar 2008 23:31:29 -0800 (PST) Received: by 10.70.19.9 with HTTP; Sun, 2 Mar 2008 23:31:29 -0800 (PST) Message-ID: <1b30d3c80803022331ga114134se96625ad24d0233e@mail.gmail.com> Date: Mon, 3 Mar 2008 08:31:29 +0100 From: "Koen Claessen" Sender: koen.claessen@gmail.com To: caml-list@yquem.inria.fr Subject: PhD positions in Functional Programming at Chalmers in Sweden In-Reply-To: <1b30d3c80801300040he01974cwe42e9a7c6204f31b@mail.gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <1b30d3c80801300040he01974cwe42e9a7c6204f31b@mail.gmail.com> X-Google-Sender-Auth: b498e073741dead9 X-Spam: no; 0.00; claessen:01 first-order:01 haskell:01 modular:01 erlang:01 model:01 real-world:01 claessen:01 winning:98 theorem:02 implemented:02 implemented:02 chalmers:02 chalmers:02 functional:02 (apologies for multiple copies) ** please forward this to interested students ** PhD Positions in Functional Programming at the department of Computer Science and Engineering at Chalmers University of Technology, Sweden http://www.cs.chalmers.se/~koen/phdad.html Application deadline: March 11, 2008 Position starts: April 1, 2008 or September 1, 2008 The PhD student will join the research activities at our department in applications of functional programming, much of which concentrates on the design and application of Domain Specific Embedded Languages. Examples of our work are QuickCheck for specification-guided random testing, and Lava for hardware design and verification. Our group has also developed the award winning automated first-order logic reasoning tools Paradox and Equinox, which are both written in Haskell. There are advertised positions in two focus areas: 1. Development of the next generation of Paradox and Equinox, which involves inventing new programming techniques for building a modular, flexible automated reasoning tool, as well as developing novel automated reasoning algorithms. As new exciting applications for automated reasoning tools arise, new demands are placed on the reasoning tools, forcing changes in how they are designed and implemented. 2. Development of verification techniques for distributed systems implemented in the functional programming language Erlang. Methods here include QuickCheck-based testing, model checking and (automated) theorem proving techniques, and integration of these different techniques. There is a possibility of attacking real-world problems from our industrial partners. For more information, please look at: http://www.cs.chalmers.se/~koen/phdad.html Koen Claessen John Hughes