[... apologies for multiple copies ... ] ************************************************************************** *** JOURNAL OF LOGIC AND COMPUTATION *** *** *** *** SPECIAL ISSUE ON *** *** MODALITIES IN CONSTRUCTIVE LOGICS AND *** *** TYPE THEORIES *** *** *** *** FIRST CALL FOR PAPERS *** *** *** *************************************************************************** TOPIC Constructive and modal logics are of foundational and practical relevance to Computer Science. Constructive logics are used as type disciplines for programming languages, as metalogics for denotational semantics, in the paradigm of program extraction from proofs and for interactive proof development in automated deduction systems such as Agda, Coq, Twelf, Isabelle, HOL, NuPrl and Plastic. Modal logics like temporal logics, dynamic logics and process logics are used in industrial-strength applications as concise formalisms for capturing reactive behaviour. Although constructive and modal frameworks have typically been investigated separately, a growing body of published work shows that both paradigms can (and should) be fruitfully combined. This special issue aims * to give a state-of-the-art snapshot of recent advances in the study of constructive modalities, * to put equal focus on the theory-oriented as well as the application-oriented approaches, and * to bring together two largely parallel communities - computer scientists with a focus on proof theory and lambda calculi, and logicians and philosphers with a focus on model theory. Topics of interest for contributions to the journal issue include, but are not limited to: * applications of intuitionistic necessity or possibility, strong monads, or evaluation modalities, * use of modal type theory to formalize mechanisms of abstraction and refinement, or to manage intensional concepts (computer science, linguistics, or the philosophy of science) in a rigorous deductive fashion * applications of constructive modal logic and modal type theory 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 * computational aspects of the Curry-Howard correspondence between lambda calculi and logics * extensions of this correspondence by other modalities or quantifiers * models of constructive modal logics such as algebraic, categorical, Kripke, topological, realizability interpretations, games semantics * notions of proof for constructive modal logics * extraction of constraints or programs, nonstandard information extraction techniques * proof search in constructive modal logic and implementations of it SUBMISSIONS Submissions must be original work, which has not been previously published in a journal and is not being considered for publication elsewhere. Manuscripts should be type written on one side only with wide margins, and not longer than 30 pages. The typing should be double-spaced. Pages should be numbered consecutively. A title page must include: full title, authors' full names and affiliations, and the address to which correspondence and proofs should be sent. Where possible, e-mail address and telephone number should be included. This should be followed by an abstract of approximately 300 words and five key words for indexing. Send a .ps or .pdf file to michael.mendler@wiai.uni-bamberg.de or post a hard copy to Michael Mendler Informatics Theory Group Faculty of Business and Applied Informatics The Otto-Friedrich University of Bamberg Feldkirchenstr. 21 D-96045 Bamberg Germany by the due date. IMPORTANT DATES Submission : February 28, 2003 Notification : April 30, 2003 Final version : June 11, 2003 CHIEF EDITOR Dov Gabbay (King's College, London) GUEST EDITORS Rajeev Gore (ANU, Australia) Michael Mendler (Bamberg University, DE) Valeria de Paiva (PARC, USA) -- Prof. Michael Mendler, PhD Universität Bamberg Professur für Grundlagen der Informatik Bamberg University Faculty of Business and Applied Informatics Informatics Theory Group Feldkirchenstraße 21 D-96045 Bamberg Germany Phone: ++49 951 863-2828 Fax: ++49 951 863-1200 E-Mail: michael.mendler@wiai.uni-bamberg.de WWW: http://www.uni-bamberg.de/wiai/gdi 21-Nov-2002 21:23:46 -0400,2230;000000000000-00000000