[TYPES] Call for papers: MoveLog05

[James Lipton]

*************** APOLOGIES FOR MULTIPLE POSTING **************


                           MoVeLog'05

         Mobile Code Safety and Program Verification
               Using Computational Logic Tools

        An ICLP Workshop, Sitges, Spain, Oct. 5, 2005

              http://babel.ls.fi.upm.es/movelog05


Computational logic and logic programming in particular can support
rich reasoning about programs, proofs, types, and specifications.

Recent breakthroughs in mobile code safety and program verification
have brought even more relevance to these tools, especially in the
areas of meta-logic proof theory, proof search, static analysis and
abstract interpretation, and model checking, even when the object code
involved is very far from declarative. Components are needed that can
perform such reasoning and the logic programming community is well
positioned to provide such components.

Especially promising has been ground-breaking work with
proof-carrying-code, a development that shows signs of having
widespread applications, and has brought a surprising number of new
challenges where computational logic can potentially contribute. It is
worth pointing out that the earliest papers in the field made explicit
mention of the possible relevance of such formalisms as lambda-prolog
and ELF for all phases of the enterprise: generation of verification
conditions, formalization of proofs, manipulation of proofs and
certificate checking.  Since then there have been proposals to combine
these approaches with other logic programming frameworks equipped with
tools for static analysis and abstract interpretation.  While other
programming paradigms may also be relevant here, logic programming may
have an important edge among other reasons because its basis in
declarative principles has led to the development of sophisticated
static analysis and abstract interpretation tools."

This workshop is aimed at using computational logic in general and
logic programming in particular to support dealing with security,
safety, correctness, and mobile code. It aims to bring together
researchers in logic programming working in mobile code safety,
security, program analysis, and correctness as well as those in
related areas of automated deduction (HOL, COQ, NuPRL, ISABELLE etc).
Relevant topics include (but are not limited to) the following:

-  Protocol analysis and verification
-  Proof Carrying Code
-  Logical Frameworks
-  Type Systems
-  Static Analysis
-  Model Checking
-  Theorem Proving
-  Proof Checking
-  Verification Condition Generation
-  Constraint Systems
-  New formal systems for verification
-  Algorithms and Cryptography Questions related to the above topics


Submissions:

Submitted papers must no be longer than 10 pages, to be presented in
~20 minutes. They must consist of original, relevant and previously
unpublished sound research results related to any of the topics of the
conference.

We also invite submissions of brief expositions of work in progress
for a poster session.  The length of these papers should be no longer
than 4 pages.

At least one author of each paper must register for the conference
before the early registration deadline. The acceptance of the paper
implies its oral presentation at the conference.


If there is sufficient interest, post-workshop proceedings will be
considered.


Dates:

- Paper Submission: July 1.
- Notification of Acceptance/Rejection: July 25.


Program Committee:

   Bruno Blanchet (ENS, Paris)
   Gopal Gupta (Univ, of Texas, Dallas, USA)
   Manuel Hermenegildo (UPM, Spain and Univ. of New Mexico, USA)
   Danny Krizanc (Wesleyan University, USA)
   *Jim Lipton  (Wesleyan University, USA and UPM, Spain)
   Julio Mariño (UPM, Spain)
   Dale Miller (École Polytechnique, INRIA Futurs, France)
   Gopalan Nadathur (University of Minnesota, USA)
   *Alwen Tiu (LORIA, Nancy, France)
   Mike Whalen (University of Minnesota, USA)

  (*)Program co-chairs


Workshop Organizing Committee:

   James Lipton, (workshop coordinator)
   Wesleyan University

   Julio Mariño Carballo
   Technical University of Madrid

   Dale Miller
   Laboratoire d'Informatique, LIX

   Manuel Hermenegildo
   Technical University of Madrid and The University of New Mexico