[TYPES] Call for Participation: MoveLog'05

[Alwen Tiu]

Apologies for multiple posting
**********************************************************************


                   CALL FOR PARTICIPATION
 
                          MoveLog05

           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/

         ICLP Home Page: http://www.iiia.csic.es/iclp2005/



REGISTRATION

Information on registration is available on ICLP website:
http://www.iiia.csic.es/iclp2005/#Registration

Early registration deadline is on 8 August, 2005.


ABOUT MOVELOG

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.


PROGRAM

9:30 Opening Comments: Jim Lipton
10:00 Invited Talk: German Puebla, Elvira Albert, Manuel Hermenegildo
       Abstract Interpretation-based Verification/Certification in the
       CiaoPP System

10:45 Break

11:15 Contributed Talks

   11:15 Alwen Tiu, Dale Miller, Gopalan Nadathur
        Mixing Finite Success and Finite Failure in an Automatic Prover

   12:00 Mario Ornaghi, Camillo Fiorentini, Alberto Momigliano
         Snapshots Generation via Constructive Logic

12:45-14:00 Lunch

   14:00 Invited Talk: Brigitte Pientka
        Tabled Higher-Order Logic Programming.

   15:00 Invited Talk: Gopalan Nadathur, TBA
   15:45 Invited Talk: Dale Miller, TBA




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 Mario (UPM, Spain)
Dale Miller (Ecole Polytechnique, INRIA Futurs, France)
Gopalan Nadathur (University of Minnesota, USA)
Mike Whalen (University of Minnesota, USA)
Alwen Tiu (LORIA, Nancy, France)

Workshop Organizing Committee

James Lipton, (program co-chair)
Wesleyan University

Alwen Tiu, (program co-chair)
Loria, Nancy

Julio Mario Carballo
Technical University of Madrid

Dale Miller
Laboratoire d'Informatique, LIX

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