FICS 2010 Contributed Talks

Abstract: We give a model for Nakano's typed lambda calculus with guarded recursive definitions in a category of metric spaces. By proving a computational adequacy result that relates the interpretation with the operational semantics, we show that the model can be used to reason about contextual equivalence.
pdf

Abstract: Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs.   Frame rules allow one to hide irrelevant parts of the state during verification, whereas the anti-frame rule allows one to hide local state from the context. We give a possible worlds semantics for Chargu{\'e}raud and Pottier's type and capability system including frame and  anti-frame rules, based on the operational semantics and step-indexed heap relations.   The worlds are constructed as a recursively defined  predicate on a recursively defined metric space, which provides a considerably simpler alternative compared to a previous construction.
pdf

Abstract: We investigate how fast modal mu-formulae may reach their fixpoints. We show a way how to construct for each ordinal number alpha less than omega^2, a formula which reaches its fixpoint in alpha steps. Our approach is based on fuses i.e. finite one--way counters, which allow us to control the number of uses of Box while iterating our formulae.
pdf

Abstract: We propose a method to characterize the fixed points described in Tarski's theorem for complete lattices. The method is proof-theoretic: the  least and greatest fixed points are ``proved''  in some inference system. We also apply the method to two other fixed point theorems, a generalization of Tarski's theorem to chain-complete  posets and  Bourbaki-Witt's theorem. Finally, we describe how the method differs from the traditional iterative method resorting to  ordinals.
pdf

Abstract: A recursive program is determined, up to bisimilarity, by the operation of the recursion body on arbitrary processes, of which it is a fixpoint.  The traditional proof of this fact uses Howe's method, but that does not tell us how the fixpoint is obtained.

In this paper, we show that the fixpoint may be obtained by a least fixpoint procedure iterated through the hierarchy of countable ordinals, using Groote and Vaandrager's notion of nested simulation.
pdf

Abstract: We show that the game and denotational semantics of a probabilistic extension of the modal mu calculus coincide.
pdf

Abstract: We present a denotational semantics for a simply typed call-by-need letrec calculus, which distinguishes direct cycles, such as "let rec x = x in x" and "let rec x = y and y = x + 1 in x", and looping recursion, such as "let rec f = \lambda x.f x in f 0".  In this semantics the former denote an exception whereas the latter denotes divergence.

The distinction is motivated by ``lazy evaluation'' as implemented in OCaml via lazy/force and Racket (formerly PLT Scheme) via delay/force: when a delayed variable is dereferenced for the first time, it is first pre-initialized to an exception-raising thunk and is updated afterward by the value obtained by evaluating the expression bound to the variable.  Any attempt to dereference the variable during the initialization raises an exception rather than diverges.  This way, lazy evaluation provides a useful measure to initialize recursive bindings by exploring a successful initialization order of the bindings at runtime and by signaling an exception when there is no such order.  It is also used for the initialization semantics of the object system in the F# programming language.

The denotational semantics is proved adequate with respect to a referential operational semantics.
pdf

Abstract: Tiling is a classic model of combinatorial structure, whose global properties are determined by simple local rules. In this paper we construct tilings with some specific properties, using self-referential argument originating in Kleene's recursion theorem. This methods proves to be very effective though the initial problems under consideration are purely combinatorial and do not refer explicitly to any questions of computability.

More specifically, we attack the problem of long range order formulated by C.Radin: whether one can determine by local rules such tilings on the plane in which we loose all information while traveling between distant areas. We present a partial answer to Radin's question by constructing a tile set τ=τ₀∪τ₁ (i.e., all tiles in τ are divided into two disjoint classes of 0-tiles and 1-tiles) such that every τ-tiling of the plane corresponds to some configuration in {0,1}^Z2, where there is no long range order.
pdf

Abstract: I show a basic Yoneda-like lemma relating strongly dinatural transformations and initial algebras. Further, I apply it to reprove known results about unique existence of uniform parameterized fixpoint operators.
pdf

Abstract: We show that: (a) Banach's and Knaster-Tarski's fixed point theorems are instances of a single theorem with a constructive proof; (b) Bourbaki-Witt's and Caristi's theorems are instances of a single theorem that cannot have a constructive proof.
pdf