This workshop on Domain Theory is held in honour of Dana Scott's 70'th birthday. The workshop is aimed at computer scientists and mathematicians who share an interest in the mathematical foundations of computer science. The workshop will focus on domains, their applications, and closely related topics. Contributions establishing connections to logic, type theory, recursion theory, and topology are welcome. Contributions on applications of domains in semantics etc. are also very welcome. Contributions will be selected based on a refereeing process. The workshop will have 6 invited talks and a number of contributed research talks of 30 minutes each.
Fixed point s play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks. The aim of the workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the fixed point operation in the different fields and formalisms.
Topics. Construction and reasoning about properties of fixed points, categorical, metric and ordered fixed point models, continuous algebras, relation algebras, fixed points in process algebras and process calculi, regular algebras of finitary and infinitary languages, formal power series, tree automata and tree languages, infinite trees, the mu-calculus and other programming logics, fixed points in relation to dataflow and circuits, fixed points and the lambda calculus, fixed points in logic programming and data bases.
Previous workshops were held in Brno (1998, MFCS workshop), Paris (2000, LC2000 workshop), Florence (2001, PLI 01 workshop).
Hybrid logic is a branch of modal logic in which it is possible to directly refer to worlds/times/states or whatever the elements of the (Kripke) model are meant to represent. Although they date back to the late 1960s, and have been sporadically investigated ever since, it is only in the 1990s that work on them really got into its stride.
It is easy to justify interest in hybrid logic on applied grounds, with the usefulness of the additional expressive power. For example, when reasoning about time one often wants to build up a series of assertions about what happens at a particular instant, and standard modal formalisms do not allow this. What is less obvious is that the route hybrid logic takes to overcome this problem (the basic mechanism being to add nominals --- atomic symbols true at a unique point --- together with extra modalities to exploit them) often actually improves the behavior of the underlying modal formalism. For example, it becomes far simpler to formulate modal tableau and resolution in hybrid logic, and completeness and interpolation results can be proved of a generality that is simply not available in modal logic. That is, hybridization --- adding nominals and related apparatus --- seems a fairly reliable way of curing many known weaknesses in modal logic. For more general background on hybrid logic, and many of the key papers, see the Hybrid Logics homepage
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 Coq and LEGO. 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. The goal of this workshop is to stimulate more systematic study of constructive or Intuitionistic Modal Logics and, in parallel of modal type theories. It aims to
Topics of interest for papers in the Workshop include, but are not limited to:
IMLA'99 was held as part of the previous FLoC.
Types support reliable reasoning in many areas such as programming languages, logic, linguistics, etc. A polymorphic type is one that stands for some number of instance types. The use of type systems for non-trivial purposes generally requires type polymorphism.
Intersection types, which were introduced roughly twenty years ago, provide type polymorphism by listing type instances. This differs from the more widely used universal types, which provide type polymorphism by giving a type scheme that can be instantiated into various type instances. (A similar relationship holds between union types and existential types, the duals of intersection types and universal types.)
Intersection types were initially intended for use in analyzing and/or synthesizing lambda models as well as in analyzing normalization properties. Over the last twenty years the scope of theoretical research on intersection types has broadened (see possible topics below). Recently, there have been a number of breakthroughs in the use of intersection types (and similar technology) for practical purposes such as program analysis.
Possible topics for submitted papers include, but are not limited to:
LFM'02 is the continuation of a series started in 1999 as a PLI affiliated workshop and continued in 2000 as a LICS affiliated workshop.
The workshop is broad in scope and covers the design of logical frameworks, meta-theoretical studies, comparative studies, implementation, and evaluation. It also covers all aspects of their use including techniques of representation of logics and languages, proofs of properties of languages, and proofs of correctness of programs. The overall aim of the workshop is to provide an understanding of the state-of-the-art of the field, to expose new research directions, and to increase the communication between the designers, implementors, and practitioners.
Logical frameworks and meta-languages are intended as a common substrate for implementing a wide variety of logics and formal systems. Their definition and implementation has been the focus of considerable work over the last decade. The underpinning of each framework or language that has been proposed is a general theory of inference systems that captures uniformities across different logics. These generalities can then be exploited in implementing systems such as theorem provers and those intended for proof and program development. Examples of logics that can be represented inside logical frameworks include higher-order logics for reasoning about high-level programming languages, logics of concurrency, modal logics, specification languages used in the design of large software systems, and formal systems describing languages. Logical frameworks themselves have been based on a variety of different languages including higher-order (intuitionistic) logics, theories of dependent types, linear logic, and modal logic. These choices lead to differences in strength in representing relevant formal systems, some of which have been examined in recent research. Work on logical frameworks and meta-languages has been supported by a variety of initiatives including several ESPRIT projects which held associated workshops.
Recently, there has also been a growing interest in logical frameworks in which it is possible to both specify and reason about the encoded logics. For frameworks that support higher-order abstract syntax, one particular challenge is to provide reasoning by induction. This task is complicated by the fact that the use of this syntax can lead to definitions for which there are no monotone inductive operators. The ability to define recursive functions inside this kind of framework is also of interest and presents similar challenges. In recent developments, a variety of new languages and techniques have been proposed which make progress in this direction. Alternative approaches include frameworks based on inductive definitions or some form of equational or rewriting logic in which substitution is explicitly encoded.
In addition to ongoing research on many of the foundational aspects mentioned above, there are numerous research groups working on systems that implement various logical frameworks and apply them to large case studies in a variety of domains. Examples of existing systems for which there is active ongoing work include Coq, Isabelle, lambdaProlog, and Twelf. An active area of research in such systems is the study of automated reasoning techniques. Current work includes the development of various automated procedures as well as the investigation of rewriting tools that use reflection or make use of links with systems that already have sophisticated rewriting systems. Program extraction and optimization are additional topics of ongoing work.
Linear logic was invented by Girard in 1986, and first appeared as a finer analysis of his denotational semantics of system F. It provides a decomposition of the connectives of intuitionistic logic (more recently also have appeared some interpretations of classical logic into linear logic). It is important to note that linear logic is not yet another exotic logic, but a canonical mathematical object, with a well structured proof-theory, even simpler than that of classical and intuitionistic logics. It is only in 1986 that linear logic was clearly formulated as a logic and armed with its, by now common, tools; but it had appeared in 1979, in categorical guise, as Barr's `star-autonomous categories'; the `exponential' construction was already present in Blass' dialog-games as early as 1972; and even as early as 1958, a non- commutative fragment of linear logic was defined by Lambek. Since its invention it has spontaneously shown up in various fields and notably in the denotational semantics of programming languages.
Linear logic, by the decomposition of intuitionistic connectives it provides, but also by the new concepts it carries (geometrization of computations, management of resources at the logical level) opens a new dimension, already intensely exploited, in applications of logic to computer science, and at the same time is the locus of a mathematical theory within which mathematics is comfortably done. It is both a theory and a tool.
New possibilities show up at two levels, which we might call the language level and the operational level. Let us say that linear logic acts as a kind of a looking-glass through which phenomena of the field are better understood.
Though only fifteen years old, linear logic has spread in the computer science and logic communities, so that it can now be considered as a mature topic. The success of various international initiatives, such as the linear logic workshops at Cornell in 1993, in Tokyo in 1996, in Marseille in 1998; the linear logic bibliography web page at Carnegie Mellon University in the U.S. and also the various European projects where linear logic played or currently plays an important role, such as the Esprit projects CLiCS and CONFER, the HCM Network "Typed Lambda-Calculus") and the current LINEAR TMR network are concrete signs of vitality of the subject. In 2002 four years will have passed since the most recent international workshop on linear logic held in 1998 in Marseille, and the time will be ripe for a successful meeting.
Martin Grohe Last modified: August 17, 2001