[TYPES] Final Call for papers: MoveLog05 (ICLP workshop)

[James Lipton]

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

        **** FINAL CALL FOR PAPERS: JULY 10 DEADLINE ****

                           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 reasoning about 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
     * Verification Condition Generation
     * Type Systems for mobile calculi and verification
     * Proof Checking
     * Applications to Mobile Code Safety and Program Verification using
       the following tools:
           o Static Analysis
           o Model Checking
           o Theorem Proving
           o Constraint Systems
     * New formal systems for verification
     * Algorithms and Cryptography Questions related to the above topics


SUBMISSIONS:

Submitted papers must be in PostScript or PDF, no longer than 10 pages
in LNCS format, to be presented in ~20 minutes. They must consist of
original, relevant and previously unpublished 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 commits one of the authors to its 
presentation at the conference.

To submit a paper, please send the paper in PS or PDF format to the
email address:

movelog05-submissions at babel.ls.fi.upm.es

You should receive a confirmation mail.

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




IMPORTANT DATES:

- Paper Submission: July 10
- Notification of Acceptance/Rejection: July 28.

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)
  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