
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.
Timetable
Time 
Sunday 
Monday 
Tuesday 
8h45 

9h30: Opening  石原 
9h45 
Aczel  Loeb 
10h45 
Gambino  Palmgren 
12h00 
Lunch 
14h45 
Pattinson  Setzer 
15h45 
Arrival in BB 
Loew  Crosilla 
16h45 
Berger  Rathjen 
18h00 
Dinner at Kloster Bräustübl 
Dinner 




Time 
Wednesday 
Thursday 
Friday 
8h45 
Negri  Sambin  Rosolini 
9h45 
Gebellato  Ciraulo  von Plato 
10h45 
Michelbrink  Carlström  Bridges 
12h00 
Lunch 
14h45 
Guided Tour Excursion Dinner 
Spitters 
Departure 
15h45 
Perdry 
16h45 
Gerhardy 
18h00 
Dinner 




Speakers & Abstracts

Peter Aczel, Manchester
Weak Constructive Set Theory
abstract

Ulrich Berger, Swansea
A strong normalization theorem based on continuous semantics
abstract

Douglas S. Bridges, Canterbury
Recent Travels in Apartness Space
abstract
The first part of this talk deals with an aspect of apartness spaces whose
nearnessspace analogue seems to be missing from the classical literature:
namely, finding a preapartness 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 preapartness 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îţă.

Jesper Carlström, Stockholm
Comments on choice in type theory
abstract

Francesco Ciraulo, Palermo
On finitary formal topologies
abstract

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.

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 prooftheoretic results come out of
these investigations.
I will review some of the wellknown connections between sets, types
and categories, and then present some recent results concerning
typetheoretic and categorytheoretic counterparts of the
constructive set theory CZF.

Silvia
Gebellato, Padova
A constructive approach to continuity by the perspective of the Basic Picture
abstract

Philipp Gerhardy, Aarhus & Darmstadt
Extracting uniform bounds from classical and semiintuitionistic 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
semiintuitionistic counterparts to the classical metatheorems, where
the semiintuitionistic setting is intuitionistic analysis extended
with certain nonconstructive principles. We discuss some advantages
and disadvantages of the classical and the semiintuitionistic
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.

石原 哉
(Ishihara Hajime), Jaist & München
A Construction of Quotient Spaces in Constructive Set Theory
abstract

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.

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 nonsequential
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
nonrecuperable error and nonlocal 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.

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 MartinLoef 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.

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 cutfree
derivations provides direct decision methods through terminating proof
search.

Erik Palmgren, Uppsala
Constructing quotient spaces
abstract

Dirk Pattinson, München
A computational Model for MultiVariable Differential Calculus
abstract
We introduce a domaintheoretic computational model for
multivariable differential calculus, which gives rise
to datatypes for differentiable functions. The model, a
continuous Scott domain for differentiable functions of n
variables, is built as a subdomain 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
domaintheoretic notion of path integral is used to extend Green's
theorem to interalvalued 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 ntuple of the derivative part. This provides an algorithm
to check consistency on the rational basis elements of the domain,
giving an effective framework for multivariable differential calculus.

Hervé Perdry, Pisa
Constructive treatments of Noetherian rings
abstract

Jan von Plato, Helsinki & München
A system of natural deduction for Heyting arithmetic
abstract

Michael Rathjen, Columbus (OSU)
Disjunction and Existence Properties for Constructive Set Theories
abstract
While Constructive ZermeloFraenkel 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.

Giuseppe Rosolini, Genova
abstract

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.

Anton Setzer, Swansea
The Π_{3}reflecting universe and extensions.
abstract

Bas Spitters, Nijmegen
Pointfree Integration Theory without Choice
abstract
In this talk I will present a choicefree and pointfree 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 frings.
Further Participants
 Josef Berger, München
 Markus Latte,
München
 Pierre Letouzey, München
 Ray Mines
 Paolo Di Muccio, Heidelberg
 Stefan Schimanski, München
 Peter Schuster, München
 Helmut Schwichtenberg, München
 Klaus Thiel, München
 Júlia Zappe,
München
