Atlas home || Conferences | Abstracts | about Atlas
Homepage: http://www.dcs.shef.ac.uk/~matt/mendler/floc-ws.html
Email: floc99imla@dcs.shef.ac.uk
Organizers: Matt Fairtlough (University of Sheffield, UK), Zhaohui Luo (University of Durham, UK), Michael Mendler (University of Passau, D), Pierangelo Miglioli (University of Milan, IT), Eugenio Moggi (University of Genova, IT), Andy Pitts (University of Cambridge, UK), Terry Stroup (University of Passau, D), Mauro Ferrari (University of Milan)
Deadline for abstracts: April 02, 1999
Description:
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.
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 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 extraction of constraints or programs, nonstandard information extraction techniques proof search in IML and implementations of IML
Date received: February 07, 1999
© 2008 Atlas Conferences Inc.