Mathematical Logic in The Netherlands
19-20 May 2011

Click here for a PDF version that contains the schedule and all abstracts.

Thursday, 19 May

10.00-11.00 Invited talk:
Henk Barendregt (University of Nijmegen)
Obtaining results accidentally
11.00-11.15 Coffee
11.15-11.40 Contributed talk:
Wim Veldman (University of Nijmegen)
Two equivalents of the fan theorem
11.40-12.05 Contributed talk:
Merlin Carl (University of Bonn)
Simplified fine structure for applications of constructibility
12.05-12.30 Contributed talk:
Yurii Khomskii (University of Amsterdam)
Regularity and definability
12.30-13.30 Lunch
13.30-14.30 Invited talk:
Jaap van Oosten (University of Utrecht)
Type theory and homotopy theory
14.30-14.55 Contributed talk:
Benno van den Berg (University of Utrecht)
A functional interpretation for non-standard arithmetic
14.55-15.20 Contributed talk:
Vieri Benci (University of Pisa), Leon Horsten (University of Bristol), and Sylvia Wenmackers (University of Groningen)
Axioms for non-archimedean probability
15.20-15.50 Coffee
15.50-16.15 Contributed talk:
Paula Henk (University of Amsterdam)
A new perspective on the arithmetical completeness of GL
16.15-16.40 Contributed talk:
Kohei Kishida (University of Groningen)
A forgotten trio: Classical semantics for first-order non-classical languages
16.40-17.05 Contributed talk:
Frank Roumen (University of Nijmegen)
Obtaining the syntactic monoid via duality
17.05-17.15 Break
17.15-18.15 Plenary discussion session about OzSL
19.00/19.30- Conference Dinner

The conference dinner takes place on Thursday, 19 May, from between 19.00 and 19.30. Click here for the venue. Registration requested.

Friday, 20 May

10.00-11.00 Invited talk:
Alessandra Palmigiano (University of Amsterdam)
Algebraic modal correspondence
11.00-11.15 Coffee
11.15-11.40 Contributed talk:
Johannes Marti (University of Amsterdam)
Relation liftings in coalgebraic modal logic
11.40-12.05 Contributed talk:
Wouter Stekelenburg (University of Utrecht)
Necessary conditions for the construction of a category of assemblies
12.05-12.30 Contributed talk:
Dion Coumans (University of Nijmegen) and Sam van Gool (University of Nijmegen)
Free algebras via partial algebras for a functor
12.30-13.30 Lunch
13.30-14.30 Invited talk:
Bas Spitters (University of Nijmegen)
Efficient real computation in constructive type theory
14.30-14.55 Contributed talk:
Lorijn van Rooijen (University of Nijmegen)
Generalised Kripke semantics for the Lambek-Grishin calculus
14.55-15.20 Contributed talk:
Jesse Alama (New University of Lisbon)
Proof analysis using fine-grained dependency information in formal mathematics
15.20-15.50 Coffee
15.50-16.15 Contributed talk:
Matteo Bianchetti (University of Milan)
Logical consequence
16.15-16.40 Contributed talk:
Tonny Hurkens (University of Nijmegen)
Logic in easy form: Four labels explaining inference
16.40-17.05 Contributed talk:
Paniel Reyes Cardenas (University of Sheffield)
Peirce's mathematical structuralism as pragmatistic realism

Abstracts of the Invited Talks

Henk Barendregt (University of Nijmegen), Obtaining results accidentally

In this talk two examples will be given. Alonzo Church was asked to prove for his dissertation that a certain problem was decidable. He could not do it, but came up with the notion of computability. On a more modest level it will be shown how I tried for my dissertation to make a recursion-theoretic model of the lambda calculus. I did not succeed, but came up with the notions of solvability and the omega-rule in lambda calculus. The latter turned out to be related to Cartesian closed categories having enough points. The former turned out to be essential for understanding Scott's models and Boehm-trees, which was an early example of co-induction.

Jaap van Oosten (University of Utrecht), Type theory and homotopy theory

In recent years, there has been a renewed interest in Martin-Löf's type theory, and most emphatically for the interpretation of Identity types as Path spaces. Around this theme there was a meeting in Oberwolfach featuring Fields medalist Vladimir Voevodsky, who is now championing a homotopy theoretical approach to type theory (and the foundations of mathematics in general). The talk will give a sketch of these developments.

Alessandra Palmigiano (University of Amsterdam), Algebraic modal correspondence

Sahlqvist correspondence theory is among the most celebrated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. Traditionally developed in a model-theoretic setting (cf. [3], [4]), it provides an algorithmic, syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames. Sahlvist result can equivalently be reformulated algebraically, via the well known duality between frames and complete atomic Boolean algebras with operators (BAO's). This perspective immediately suggests generalizations of Sahlqvist's theorem along algebraic lines, e.g. to the cases of distributive [2] or arbitrary lattices with operators. We illustrate, by way of examples, the algebraic mechanisms underlying Sahlqvist correspondence for classical modal logic [1], after having discussed the appropriate duality with the relational semantics. We show how these mechanisms work in much greater generality than the classical setting in which Sahlqvist theory was originally developed. Next we present the newly developed algorithm ALBA [2] which effectively extends the existing most general results on correspondence.
[1] W. Conradie, A. Palmigiano, S. Sourabh, Algebraic Sahlqvist Correspondence, in preparation.
[2] W. Conradie and A. Palmigiano, Algorithmic Correspondence and Canonicity for Distributive Modal Logic, submitted.
[3] H. Sahlqvist, Correspondence and completeness in the first and second-order semantics for modal logic, in Proceedings of the 3rd Scandinavian Logic Symposium, Uppsala 1973, S. Kanger, ed., 1975, pp. 110-143.
[4] J. van Benthem, Modal logic and classical logic, Bibliopolis, Napoli, 1983.

Bas Spitters (University of Nijmegen), Efficient real computation in constructive type theory

In 1967 Bishop proposed to use constructive analysis as a language for exact real computations. Martin Löf proposed constructive type theory as an actual programming language. This language now forms the base of both proof assistants and programming languages. I will report on our effort to actually carry out this research program: we provide an efficient computer verified implementation of exact real numbers in the Coq proof assistant.