| | All
sessions take place in auditorium 2.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. |
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. |
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. |
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. |
| |