[TYPES/announce] MALOA PhD position in logic at ENS Lyon

[Olivier Laurent]

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


   *
   *   *
   *   PhD Position in Logic at ENS Lyon (MALOA project)   *
   *   *
   *   *
   *   October 1st, 2010 -- September 30th, 2013   *
   *   *
   *

MALOA (From MAthematical LOgic to Applications) is a European
Initial Training Network:

   http://www.logique.jussieu.fr/MALOA/

Amongst the proposed PhD positions, one will be open in the
Plume team of the computer science laboratory of the ENS Lyon
(France).

   http://www.ens-lyon.fr/LIP/PLUME/


The main research topics of the team are:
  * Proof theory and computer science
  * Curry-Howard correspondence
  * Programming languages semantics
  * Linear logic, game semantics, realisability
  * Implicit computational complexity
  * Concurrency theory
  * Computer assisted reasoning

Applications are now open. Submissions including :
  * a detailed curriculum vitae
  * a list of topics of interest
  * the names and e-mail addresses of two references
should be sent by e-mail to olivier.laur...@ens-lyon.fr by
April 30th, 2010.

Before applying, please check you satisfy the eligibility
conditions:
   http://www.logique.jussieu.fr/MALOA/Eligibility.html

Important dates:
   * applications:  April 30th,  2010
   * starting date: October 1st, 2010

Do not hesitate to contact us if you want some additional
informations:
   olivier.laur...@ens-lyon.fr



-- 
Olivier LAURENT
e-mail : olivier.laur...@ens-lyon.fr
www: http://perso.ens-lyon.fr/olivier.laurent/

[TYPES/announce] CFP: Call for papers, Coq Workshop (deadline March 22nd)

[Yves Bertot]

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

lease help disseminate this call for papers

Two changes in the call for papers:

1/ papers describing experiments in other type theory-based proof 
assistants are explicitly invited to this workshop,

2/ EPTCS (http://eptcs.org/) has agreed to host the proceedings.

Call for papers

The Coq workshop will bring together Coq users, developers and 
contributors. The workshop will be organized from submitted papers, 
invited talks and a plenary discussion on the evolution and design of 
Coq. Topics for submitting a paper include:

   * Experiments with type-theoretic proof assistants
   * Language or tactics features
   * Theory and implementation of the Calculus of Inductive Constructions
   * Applications and experience in education and industry
   * Tools, platforms built on Coq
   * Plugins, libraries for Coq
   * Interfacing with Coq
   * Formalization tricks and Coq pearls

Authors should submit their paper through EasyChair at the following link:

http://www.easychair.org/conferences/?conf=coq2

Submitted papers should be in (postscript or) portable document format. 
Papers should not exceed 12 pages in length in single-column full-page 
11pt A4 style.

If there is sufficient demand, we will try to organize a time slot for 
demonstrations. Similarly, we may also organize a session on the lessons 
learned from teaching Coq. If you are interested, please send a brief 
proposal.

Venue

FLoC 2010, Edinburgh, Scotland

Important Dates

   * March 22nd: Deadline for submission of papers
   * May 1st: Acceptance Notification
   * May 31st: Final version of articles
   * July 9th: Workshop in Edinburgh

Program Committee

   * Andrew Appel
   * Yves Bertot (Chair)
   * Adam Chlipala
   * Georges Gonthier
   * Benjamin Grégoire
   * Hugo Herbelin
   * Micaela Mayero
   * Christine Paulin-Mohring
   * Bas Spitters


Contact

yves.ber...@sophia.inria.fr