CLM 2004



Printer friendly


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.

Time Sunday Monday Tuesday
8h45 9h30: Opening石原
9h45 AczelLoeb
10h45 GambinoPalmgren
12h00 Lunch
14h45 PattinsonSetzer
15h45 Arrival
16h45 BergerRathjen
18h00 Dinner at
Kloster Bräustübl
Time Wednesday Thursday Friday
8h45 NegriSambinRosolini
9h45 GebellatoCiraulovon Plato
10h45 MichelbrinkCarlströmBridges
12h00 Lunch
14h45 Guided Tour
Spitters Departure
15h45 Perdry
16h45 Gerhardy
18h00 Dinner

Speakers & Abstracts

  1. Peter Aczel, Manchester

    Weak Constructive Set Theory

  2. Ulrich Berger, Swansea

    A strong normalization theorem based on continuous semantics

  3. Douglas S. Bridges, Canterbury

    Recent Travels in Apartness Space
    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 YX that provides the right setting for proximal convergence (which is normally defined in an ad hoc way with no reference to any apartness on YX. We deal with two pre--apartness structures on YX, 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

  5. Francesco Ciraulo, Palermo

    On finitary formal topologies

  6. Laura Crosilla, Firenze

    Explicit constructive set theory
    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
    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

  9. Philipp Gerhardy, Aarhus & Darmstadt

    Extracting uniform bounds from classical and semi-intuitionistic proofs
    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

  11. Iris Loeb, Nijmegen

    Equivalents of The (Weak) Fan Theorem
    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
    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
    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
    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

  16. Dirk Pattinson, München

    A computational Model for Multi-Variable Differential Calculus
    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

  18. Jan von Plato, Helsinki & München

    A system of natural deduction for Heyting arithmetic

  19. Michael Rathjen, Columbus (OSU)

    Disjunction and Existence Properties for Constructive Set Theories
    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


  21. Giovanni Sambin, Padova

    On the meaning of definitions in formal topology and the basic picture
    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 Π3-reflecting universe and extensions.

  23. Bas Spitters, Nijmegen

    Point-free Integration Theory without Choice
    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
Josef Berger Peter Schuster Klaus Thiel