[... This message was sent to several mailing lists: apologies to those of you who receive multiple copies. Please forward it to everyone who might be interested ... ] ----------------------------------------------------------------------- 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/ -----------------------------------------------------------------------