[Prev][Next][Index][Thread]

2nd CFP: Intuitionistic Modal Logic and Applications


                      WORKSHOP  ANNOUNCEMENT 

                  *** SECOND CALL FOR PAPERS ***

-----------------------------------------------------------------------


  FLoc'99 Workshop         (affiliated to LICS'99)

  IMLA: Intuitionistic Modal Logic and Applications

  July 6, 1999
  Trento, Italy


BACKGROUND

  Intuitionistic and modal logics are of foundational relevance to
  Computer Science and both have led to successful applications in the
  formal specification and verification of computer systems. The
  intuitionistic and the modal frameworks are usually investigated
  separately.  However, a growing body of published work, stimulated by
  theoretical considerations and fed by various applications in Computer
  Science, shows that both paradigms may fruitfully be merged.

  Intuitionistic modal logic (IML) and modal type theory (MTT) can exploit
  both the proof-theoretic strengths of intuitionistic logic and the
  model-theoretic features of modal logics. The potential and the
  challenge of IML and MTT both lie in finding a satisfactory combination
  of its intensional and its extensional aspects.  We intend this one-day
  workshop to seed a more concerted organisation of the ongoing research
  in the area of IML, bringing together the method-oriented and the
  problem-oriented approaches on the one hand, and the proof-theoretic and
  model-theoretic ones on the other. This will create fruitful research
  stimuli through the friction between engineering applications and pure
  theory, and between intensional and extensional lines of thinking.


TOPICS OF INTEREST

  Contributions are invited on all aspects of the theory and application
  of IML and MTT.  Topics of interest include, but are not limited to:

  * applications of intuitionistic necessity or possibility,
    strong monads, or evaluation modalities

  * use of IML and MTT to formalize mechanisms of abstraction
    and refinement

  * applications of IML and MTT to formal verification, abstract
    interpretation, and program analysis and optimization

  * applications of modal types to integration of inductive and
    co-inductive types, higher-order abstract syntax, strong 
    functional programming

  * extraction of constraints or programs, nonstandard information
    extraction techniques

  * Curry-Howard correspondence between computational lambda
    calculi and computational logics

  * extensions of this correspondence by other modalities or
    quantifiers

  * models of IML such as algebraic, categorical, Kripke, topological,
    realizability interpretations

  * notions of proof for IML and intermediate constructive logics

  * proof search in and implementations of IML


FORMAT

  The workshop will be an informal one-day meeting with invited
  talk, regular paper presentations, and discussion. 


INVITED SPEAKER 

  Frank Pfenning (Pittsburgh)


PUBLICATION

  The final versions of all workshop papers will be made available on the
  workshop web page. Authors of accepted papers will be invited to submit
  full and revised versions for a special journal issue of Mathematical
  Structures in Computer Science (MSCS) dedicated to the topic of the
  workshop. There will be a second round of refereeing for MSCS according to
  high journal standards.


SUBMISSIONS

  There is no page limit for workshop contributions, which may
  be in the form of extended abstracts, or draft full papers. Workshop 
  contributions to be considered for MSCS must be original work that 
  has not yet appeared elsewhere. Submissions should be sent to 
  floc99imla@dcs.shef.ac.uk (preferred route) or directly to

  Matt Fairtlough                 email: m.fairtlough@dcs.shef.ac.uk
  The University of Sheffield     phone: +44 (0) 114 22 21826
  Department of Computer Science  fax:   +44 (0) 114 22 21810
  Regent Court
  211 Portobello Street
  Sheffield S14 DP
  U.K.

  or one of the other workshop organisers by April 2, 1999.  For more 
  information on submissions and addresses see the IMLA workshop web 
  page (address below).

IMPORTANT DATES 

  IMLA submission deadline: April 2, 1999
  IMLA notification       : May 21, 1999
  IMLA final version      : June 11, 1999

  submission deadline for full and revised MSCS journal versions: 
  Winter 1999, to be announced (check IMLA web page)

PROGRAMME COMMITTEE

  Matt Fairtlough (Sheffield)
  Zhaohui Luo (Durham)
  Michael Mendler (Sheffield)
  Pierangelo Miglioli (Milan)
  Eugenio Moggi (Genova)
  Andy Pitts (Cambridge)
  Terry Stroup (Passau)

ORGANISERS

  Mauro Ferrari (Milan)
  Matt Fairtlough (Sheffield)
  Michael Mendler (Passau)

WORKSHOP WEB PAGE

  http://www.dcs.shef.ac.uk/~matt/mendler/floc-ws.html
  
  The FLoC'99 page is at 
  http://www.cs.bell-labs.com/cm/cs/what/floc99/

-----------------------------------------------------------------------