CLM 2004

• Home
• Directions
• Photos
• Programme

Programme

Printer friendly
PDF

Schedule

Each speaker will have 45 minutes for their presentation. Between two lectures there will be a break of 15 minutes for questions and scene changing. Lectures start at 8h45 in the morning.

Speakers & Abstracts

1. Peter Aczel, Manchester

   Weak Constructive Set Theory
   abstract
   

2. Ulrich Berger, Swansea

   A strong normalization theorem based on continuous semantics
   abstract
   

3. Douglas S. Bridges, Canterbury

   Recent Travels in Apartness Space
   abstract
   The first part of this talk deals with an aspect of apartness spaces whose nearness--space analogue seems to be missing from the classical literature: namely, finding a pre--apartness structure on Y^X that provides the right setting for proximal convergence (which is normally defined in an ad hoc way with no reference to any apartness on Y^X. We deal with two pre--apartness structures on Y^X, where X is an inhabited set and Y a uniform space, in order to clarify the connection between proximal and uniform convergence. In the second part of the talk we introduce two notions of connectedness for apartness spaces, and discuss various fundamental properties of connected sets. All the work presented was carried out very recently by the speaker and L.S. Vîţă.

4. Jesper Carlström, Stockholm

   Comments on choice in type theory
   abstract
   

5. Francesco Ciraulo, Palermo

   On finitary formal topologies
   abstract
   

6. Laura Crosilla, Firenze

   Explicit constructive set theory
   abstract
   We shall introduce weak systems of constructive set theory with urelements which also embody a notion of (self applicable) operation.
   The resulting set theories are proof theoretically weak but allow for inductive constructions, being therefore of interest for carrying out metatheoretical studies. The systems can also be seen as a bridge between two distinct traditions of foundations for constructive mathematics, mainly between constructive versions of Zermelo Fraenkel set theory and Feferman's explicit mathematics.

7. Nicola Gambino, Cambridge

   On Relating Sets, Types and Categories
   abstract
   Set theory, type theory, and category theory have all been considered as interesting foundational contexts for the development of constructive mathematics. Much recent research focuses on relating the three settings, and nice proof-theoretic results come out of these investigations. I will review some of the well-known connections between sets, types and categories, and then present some recent results concerning type-theoretic and category-theoretic counterparts of the constructive set theory CZF.

8. Silvia Gebellato, Padova

   A constructive approach to continuity by the perspective of the Basic Picture
   abstract
   

9. Philipp Gerhardy, Aarhus & Darmstadt

   Extracting uniform bounds from classical and semi-intuitionistic proofs
   abstract
   Using monotone proof interpretations, Kohlenbach proved very general logical metatheorems for the extraction of effective uniform bounds from classical, ineffective proofs in functional analysis, covering arbitrary abstract metric and normed linear spaces. We present semi-intuitionistic counterparts to the classical metatheorems, where the semi-intuitionistic setting is intuitionistic analysis extended with certain non-constructive principles. We discuss some advantages and disadvantages of the classical and the semi-intuitionistic approach respectively and sketch some additional recently developed extensions. Finally, we illustrate the use of these metatheorems by a simple example from metric fixed point theory.

10. 石原 哉 (Ishihara Hajime), Jaist & München

    A Construction of Quotient Spaces in Constructive Set Theory
    abstract
    

11. Iris Loeb, Nijmegen

    Equivalents of The (Weak) Fan Theorem
    abstract
    The talk will start with an overview of the goals of different kinds of reverse mathematics: classical, informal constructive and formal constructive. Then it will focus on formal constructive reverse mathematics and the (weak) fan theorem.

12. Tobias Löw, Darmstadt

    A Universal Model for the sequential languages in Locally Boolean Domains
    abstract
    The main reason, why it is so hard to find fully abstract models for the language PCF, comes from the fact, that PCF is sequential while its standard domain model contains non-sequential elements like the parallel or.
    In 1994 Cartwright, Curien and Felleisen solved the full abstraction problem for the language SPCF, an extension of PCF. They added an non-recuperable error and non-local catch operators to the language and showed that the model in the category of sequential data structures and observably sequential functions is fully abstract.
    About 2 years ago Jim Laird introduced locally boolean domains (lbd), a new kind of domains providing a fully abstract model for SPCF. One can show that lbds also provide a universal model for infinitary SPCF (i.e. with recursive types and infinite terms) and that type 1 over the natural numbers is universal for lbds.
    Infinitary SPCF hosts the recursive type D ˜ D^ω → Σ which provides a model for infinitary CPS target language (sort of an infinitary λ-calculus). It can be shown that every term of SPCF can be ``realized'' by an object of D that can be denoted by a term of
    the infinitary CPS language. From this it follows that every object of D appears as denotation of an appropriate term of infinitary CPS, i.e. that D is a universal model.
    However, the model is not ``fully complete'' because different infinite normal forms receive the same interpretation in D. This suggests that λ-calculus is not the optimal representation of sequential algorithms or, rather, that the model D might give rise to an optimizing translation.
    This is joint work with Prof. Thomas Streicher.

13. Markus Michelbrink, Swansea

    Interfaces as games, programs as strategies
    abstract
    Peter Hancock and Anton Setzer developed the notion of interface to introduce interactive programming into dependent type theory. We generalise their notion and get an even simpler definition for interfaces. With this definition the relationship of interfaces to games becomes apparent. In fact from a game theoretical point of view interfaces are nothing than special games. Programs are strategies for these games. There is an obvious notion of refinement which coincides exactly with the intuition of what a refinement should do. Interfaces together with the refinement relation build a complete lattice (without least and greatest element) in the sense that every family of interfaces has a least common refinement and there is an interface such that all members of this family refine this interface and this interface is an refinement for every other interface with this property. A program/ strategy on a refinement of an interface gives a strategy on the interface. We can define several operators on interfaces: tensor, par, choice, bang et cetera. Every notion has a dual notion by interchanging the viewpoint of player and opponent. Lollipop is defined as usual in terms of tensor and negation. We define the notion of fair strategy on A ⊸ B. A fair strategy is essentially a pair of a strategy and a proof that this strategy plays in both games eventually. By a slight restriction of the notion of interface we are able to define a composition for fair strategies on A ⊸ B and B ⊸ C. The obtained strategy is again fair. We can define fair strategies on A ⊸ A and A ⊗ (A ⊸ B) ⊸ B. These strategies are versions of copy cat strategies. Identifying strategies by some kind of behavioural equivalence we expect to receive a linear category. However we have not checked all details until now. All results so far can be achieved in intensional Martin-Loef Type Theory and are verified in the theorem prover Agda. There are numerous links to other areas including refinement calculus, linear logic, game semantics, formal topology, process algebra, model checking and so on. However we have not explored all these relationships until now but intend to do so in the future.

14. Sara Negri, Helsinki & München

    Formal Kripke semantics with applications
    abstract
    A system of sequent calculus is presented in which the Kripke semantics of intuitionistic logic is part of the formal syntax. Axioms for Kripke frames are converted into rules extending the basic sequent calculus. The method can be applied to modal logic, provability logic, intermediate logics, etc. Admissibility of structural rules (weakening, contraction, and cut) for standard systems of modal logic follows from the general result for extensions of sequent calculus with rules. Analysis of cut-free derivations provides direct decision methods through terminating proof search.

15. Erik Palmgren, Uppsala

    Constructing quotient spaces
    abstract
    

16. Dirk Pattinson, München

    A computational Model for Multi-Variable Differential Calculus
    abstract
    We introduce a domain-theoretic computational model for multi-variable differential calculus, which gives rise to data-types for differentiable functions. The model, a continuous Scott domain for differentiable functions of n variables, is built as a sub-domain of the product of n+1 copies of the function space on the domain of intervals by tupling together consistent information about locally Lipschitz (piecewise differentiable) functions and their differential properties (partial derivatives). We show, in two stages, that consistency is decidable on basis elements. First, a domain-theoretic notion of path integral is used to extend Green's theorem to interal-valued vector fields and show that integrability of the derivative information is decidable. Then, we use techniques from the theory of minimal surfaces to construct the least and the greatest piecewise linear functions that can be obtained from a tuple of n+1 rational step functions, assuming the integrability of the n-tuple of the derivative part. This provides an algorithm to check consistency on the rational basis elements of the domain, giving an effective framework for multi-variable differential calculus.

17. Hervé Perdry, Pisa

    Constructive treatments of Noetherian rings
    abstract
    

18. Jan von Plato, Helsinki & München

    A system of natural deduction for Heyting arithmetic
    abstract
    

19. Michael Rathjen, Columbus (OSU)

    Disjunction and Existence Properties for Constructive Set Theories
    abstract
    While Constructive Zermelo-Fraenkel Set Theory, CZF, has gained the status of a standard reference theory for developing constructive predicative mathematics, surprisingly little is known about certain pleasing metamathematical properties such as the disjunction and the numerical existence property which are often considered to be hallmarks of intuitionistic theories. The talk will be concerned with these properties and will introduce a new realizability notion to settle them.

20. Giuseppe Rosolini, Genova

    
    abstract
    

21. Giovanni Sambin, Padova

    On the meaning of definitions in formal topology and the basic picture
    abstract
    Some changes in the original definition of formal topology have been introduced recently: mainly, the positivity predicate has been extended into a positivity relation and the positivity axiom has been dropped. Moreover, all other notions, notably continuous relations and formal points, have been adjusted accordingly. Several arguments, both of conceptual and of technical nature, show that these changes, which contingently have been induced by the discovery of the basic picture, are actually necessary for a proper development of topology in a predicative foundation and that they are very useful in any case. In this talk, I will collect all these arguments and try to give a unified view, which includes new notions like overlap algebras and bases for closed subsets.

22. Anton Setzer, Swansea

    The Π₃-reflecting universe and extensions.
    abstract
    

23. Bas Spitters, Nijmegen

    Point-free Integration Theory without Choice
    abstract
    In this talk I will present a choice-free and point-free development of parts of Bishop's integration theory, culiminating in an easy proof of the spectral theorem. This proof is based on Coquand's constructive version of the Stone representation theorem combined with some elementary theory of f-rings.

Further Participants

1. Josef Berger, München
2. Markus Latte, München
3. Pierre Letouzey, München
4. Ray Mines
5. Paolo Di Muccio, Heidelberg
6. Stefan Schimanski, München
7. Peter Schuster, München
8. Helmut Schwichtenberg, München
9. Klaus Thiel, München
10. Júlia Zappe, München