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
Peter Aczel, Manchester
Weak Constructive Set Theory
Ulrich Berger, Swansea
A strong normalization theorem based on continuous semantics
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îţă.
Jesper Carlström, Stockholm
Comments on choice in type theory
Francesco Ciraulo, Palermo
On finitary formal topologies
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)
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
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
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.
A constructive approach to continuity by the perspective of the Basic Picture
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.
(Ishihara Hajime), Jaist & München
A Construction of Quotient Spaces in Constructive Set Theory
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)
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.
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
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
Erik Palmgren, Uppsala
Constructing quotient spaces
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.
Hervé Perdry, Pisa
Constructive treatments of Noetherian rings
Jan von Plato, Helsinki & München
A system of natural deduction for Heyting arithmetic
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.
Giuseppe Rosolini, Genova
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.
Anton Setzer, Swansea
The Π3-reflecting universe and extensions.
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.
- Josef Berger, München
- Markus Latte,
- 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,