IMLA on Friday

Detailed program
Friday July 26th, 2002
See also the unified by-slot program

All sessions take place in auditorium 2.

Session 1

08:50-09:00  Opening

09:00-10:00  Dana Scott, Carnegie Mellon U, USA
Invited talk: Realizability and modality
Intuitionistic logic admits a richer range of modal operators than classical logic. Some examples will be explained via realizability models for type theory.

10:00-10:30  Steve Awodey, Carnegie Mellon U, USA
Andrej Bauer, U Ljubljana, Slovenia
Propositions as [types]
We consider a modal operator [A] on types for erasing computational content and formalizing a notion of proof irrelevance. We give rules for such bracket types in dependent type theory and provide complete semantics using regular categories and topological models. We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with intuitionistic first-order logic.

Session 2

11:00-11:30  Claudio Hermida, IST Lisbon, Portugal
A categorical outlook on relational modalities and simulations
We characterise bicategories of spans, relations and partial maps universally in terms of factorisations involving maps. We apply this characterisation to show that the standard modalities [] and <> arise canonically as the extension of a predicate logic from functions to (abstract) relations. With the resulting fibrational interpretation of modalities, we show how to deal with representabilitiy, thereby deriving logical predicates for the power-object and partial-map-classifier monads. In the second part of the article, we exhibit an intrinsic relationship between satisfaction of modal formulae (in a transition system) and simulations, and apply it to exhibit the role of the biclosed nature of the bicategory of relations in proving that observational similarity implies similarity.

11:30-12:00  Gianluigi Bellin, U Verona, Italy
Towards a formal pragmatics: An intuitionistic theory of assertive and conjectural judgements with an extension of Gödel, McKinsey and Tarski's S4 translation.
Formal pragmatics extends classical logic to characterise the logical properties of the operators of illocutionary force such as those expressing assertions and obligations. Here we consider the cases of assertions and hypothetical (or conjectural) judgements: for a mathematical proposition A, the assertion of A is justified by the availability of a proof of A, while conjectural assertion is justified by the the absence of a refutation of A. We give a unitary sequent calculus with subsystems characterizing intuitionistic and a fragment of classical reasoning with such operators. Extending Gödels's and McKinsey and A. Tarski's translation of intuitionistic logic into S4, we prove soundness and completeness of our sequent calculus with respect to the S4 semantics.

12:00-12:30  Olivier Brunet, INRIA Rhône-Alpes, France
A modal logic for observation-based knowledge representation
In this paper we introduce and explore ways to include a notion of partiality of information in knowledge representation formalisms. This leads to the definition of an algebraic structure based on the notion of observation and partial representation, and study the logical behaviour of those structures.

Session 3

14:00-15:00  Giovanni Sambin, U Padova, Italy
Invited talk: Open truth and closed falsity
The new theory which I have called the basic picture, and which is a structural approach to basic notions of topology via symmetry and logical duality, lends itself also as a very natural constructive semantics for intuitionistic temporal logics, in which both open subsets and closed subsets are used to interpret formulae.

15:00-15:30  J. M. Davoren, Australian National U
V. Coulthard, Australian National U
T. Moor, Australian National U
Rajeev P. Goré, Australian National U
A. Nerode, Cornell U, USA
Topological semantics for intuitionistic modal logics, and spatial discretisation by A/D maps
The contribution of this paper is threefold. First, we take the well-known Intuitionistic modal logic of Fischer-Servi with semantics in birelational Kripke frames, and give the natural extension to topological Kripke frames where the frame conditions relating the Intuitionistic partial order with the modal relation generalise to semi-continuity properties of the relation with respect to the topology. Second, we develop the theory of an interesting class of topologies arising from spatial discretisation by finitary covers; the motivating case is covers of Euclidean space. We use the name "A/D map" to designate covers of a space whose cover cells do not generate any infinite descending chains; for analog-to-digital conversion, were one seeks a discretised view of a continuous world via the cells of a cover, the limits of discernment should be finite. Third, we give a novel application of Intuitionistic semantics to the problem of approximate model-checking of classical modal formulas in models where the exact evaluation of denotation sets is not possible; such models are the norm in applications of modal logics to the formal analysis and design of hybrid (mixed continuous and discrete) dynamical systems. The main result of the paper is that for the positive fragment of a modal language generated from a finite set of atomic propositions, we can give general lower and upper bounds on the classical denotation set of a formula in a given model. Moreover, these bounds are the Intuitionistic denotation sets of the same formula in two different models, where the lower and upper Intuitionistic models are built from an A/D map and have finitary quotients.

Session 4

16:00-16:30  Maria Emilia Maietti, U Padova, Italy
Eike Ritter, U Birmingham, UK
Modal run-time analysis revisited
To perform run-time analysis we present an implicit modal type system as a variation of Davies and Pfenning's modal one. We replace the use of the modality by adding a new arrow type to abstract on a compile-time assumption. For it we provide both a categorical semantics and an operational semantics with a two stage evaluation.

16:30-17:00  Discussion