Contents & Abstracts, Schedae Informaticae, Issue 12 (2003)

Pierre Lescanne , Explicit Substitutions and Intersection Types, pp. 11-15

         Full version:

Paweł Waszkiewicz , Domain Theory as a Tool for Topology - a Case Study, pp. 17-26

Abstract.  In this paper we adopt a certain view on continuous posets and see them as models of their spaces of maximal elements, which are most often topologies rich in structure. Adopting this perspective seems to be fruitful: we are often able to match structural properties of the modelling poset to properties of the modelled space. It was discovered by Mike Reed and Keye Martin two years ago that existence of a measurement on the model corresponds to existence of a development for the modelled topological space. We present an elementary proof of this fact and show how one can use this result to give a new proof to one of the first metrization theorems in Topology.

Keywords.  Continuous dcpo, domain, development, metrization.

Full version:

René David , Karim Nour , A Short Proof of the Strong Normalization of the Simply Typed lm-calculus, pp. 27-33

Abstract.  We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed lm-calculus.

Full version:

Mariangiola Dezani-Ciancaglini , Silvia Ghilezan , A Behavioural Lambda Model, pp. 35-47

Abstract.  We build a lambda model which characterizes completely (persistently) normalizing, (persistently) head normalizing, and (persistently) weak head normalizing terms. This is proved by using the finitary logical description of the model obtained by defining a suitable intersection type assignment system.

Keywords.  Lambda calculus, intersection types, models of lambda calculus, Stone duality.

Full version:

Abstract.  Positive recursive (fixpoint) types can be added to the polymorphic  (Church-style) lambda calculus l2 (System F) in several different  ways, depending on the choice of the elimination operator. Known extensions of l2 fall into two equivalence classes with  respect to mutual interpretability by means of beta-eta reductions, and  elimination operators for fixpoint types  can be classified accordingly as either "iterators" or "recursors".  Systems with iterators can be defined within l2  by means of beta reductions, and it is conjectured that systems with recursors  cannot.  In this paper we define the general form of mutual iteration scheme in l2 and  we show that the explicit solution for particular functions defines recursors within l2, though proof of this fact requires much more than beta reductions, namely parametricity.  We propose a convenient equational inference rule which can be used instead of  parametricity for proving equational properties of polymorphic functions,  defined by iterators.

Keywords. Typed lambda calculus, inductive definitions, equational reasoning. 

Full version:

Noël Bernard , Investigating the Logical Aspects of the Pi-calculus, pp. 57-66

Abstract.  The relations between the p-calculus and logic have been less extensively studied than for the l-calculus. We give an account on what can be found in the literature, in two distinct directions: model-checking, and typing. We propose a Curry-Howard correspondence taking into account the dynamic properties of the p-calculus. This is a first presentation of a work in progress.

Keywords.  p-calculus, model-checking, m-logic, proof theory, Curry-Howard correspondence 

Full version:

Yves Bertini, About the Notion of Easiness in l-Calculus, pp. 67-75

Abstract.  We recall some syntactic techniques used to prove the consistency of some extensions of the l-calculus. These techniques are a possible way to prove the easiness of YΩ₃.

Keywords.  Easy-terms, consistency, notion of undefined, infinite l-calculus.

Full version:

Daniel Hirschkoff , Étienne Lozes , Davide Sangiorgi , Separability, Expressiveness, and Decidability in the Ambient Logic, pp. 77-84

Abstract.  The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (= _L ). We consider MA, and two Turing complete subsets of it, and , respectively defined by imposing a semantic and a syntactic constraint on process prefixes. The main contributions include: coinductive and inductive operational characterisations of  = _L; an axiomatisation of  = _L on ; the construction of characteristic formulas for the processes in with respect to = _L; the decidability of = _L on and on , and its undecidability on MA.

Keywords.  Mobile Ambients, spatial logics, modal logics, intensionnality, characteristic formulas.

Full version:

Paweł M. Idziak , Classification in Finite Model Theory, pp. 85-95

          Full version:

Christophe Raffalli , System ST, pp. 97-112

Abstract.  This article is a set of commented slides presenting a new type system: "System ST" (ST stands for SubTyping), based on subtyping. The extraordinary expressive power of the system (not really visible in this set of slides) leads us to think that it could be a good candidate for doing both proofs and extractions of programs. The main argument to support this claim is the completeness of the system which says that if a program can be proved correct (using realizability), then it can be extracted from a proof.

Full version:

David Teller , Pascal Zimmer , Daniel Hirschkoff , Using Ambients to Control Resources (short abstract), pp. 113-127

Abstract.  Current software and hardware systems, being parallel and reconfigurable, raise new safety and reliability problems, and the resolution of these problems requires new methods. Numerous proposals attempt at reducing the threat of bugs and preventing several kinds of attacks. In this paper, we develop an extension of the calculus of Mobile Ambients, named Controlled Ambients, that is suited for expressing such issues, specifically Denial of Service attacks. We present a type system for Controlled Ambients, which makes resource control possible in our setting.

Full version:

Marek Zaionc , Asymptotic Properties of Logics, pp. 129-138

Abstract.  This paper presents the number of results concerning problems of asymptotic densities in the variety of propositional logics. We investigate, for propositional formulas, the proportion of tautologies of the given length n against the number of all formulas of length n. We are specially interested in asymptotic behavior of this fraction. We show what the relation between a number of premises of an implicational formula and asymptotic probability of finding a formula with this number of premises is. Furthermore we investigate the distribution of this asymptotic probabilities. Distribution for all formulas is contrasted with the same distribution for tautologies only.

Keywords.  Propositional logic, asymptotic density of tautologies, probabilistic methods in logic.

Full version: