Project workshops and conferences:

Correctness by Construction CORCON 2014 Workshop
(2427 March 2014) Università degli Studi di GenovaThis workshop aims at bringing together the participants and those researchers who are interested in the themes of the project.
Related workshops and conferences:

JAIST Logic Workshop Series 2015: Constructivism and Computability
(26 March 2015) Shiinoki Cultural Complex, Kanazawa, JapanIn 2015, JAIST Logic Workshop Series focuses on “Constructivism and Computability” aiming at interaction and knowledge transfer between constructive mathematics and computability theory. The workshop is held being affiliated with EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.unitrier.de/) and CORCON (https://corcon.net/), but is open to all researchers in the areas. See the announcement for further details.

Workshop on Applications on Fibrations in Computer Science (FIBS2014)
(2324 June 2014) University of StrathclydeThe idea of the workshop is to get people using fibrational methods in computer science together to catch up with what each of us is doing, to learn from each others techniques and to possibly chart ideas for future development and interaction.

Computability Theory and Foundations of Mathematics 2014 (CTFM2014)
(1720 February 2014) Tokyo Institute of TechnologyIt is a workshop to develop computability theory and logical foundations of Mathematics, and it aims to provide participants with the opportunity to exchange ideas, information and experiences on active and emerging topics in logic, including but not limited to: Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory.

JAIST Logic Workshop Series 2014: Kanazawa Workshop for Dynamic Epistemic Logics
(2122 February 2014) Shiinoki Cultural ComplexKanazawa Workshop for Dynamic Epistemic Logics is organized by Satoshi Tojo and Katsuhiko Sano of Japan Advanced Institute of Science and Technology (JAIST) from 21st to 22nd February, 2014. The aim of the Workshop is to discuss about (dynamic) epistemic logic and its application from theoretical and practical viewpoints.
Project seminars:

Canberra, Australian National University: Streams in a minimalist foundation
(23 January 2014) 15:00Professor Giovanni Sambin, from the Università degli Studi di Padova, Italy, visiting ANU, will speak about streams in the minimalist foundation of Mathematics.

Logic Seminar at Australian National University: Why topology must be point free
(4 February 2014) 15:00Dr Maria Emilia Maietti, from the Università degli Studi di Padova, Italy, visiting ANU, will introduce her research on Formal Topology.

JAIST Logic Workshop Series 2014: Computational content of proofs
(57 March 2014) JAIST, Lecture room I1, 15:1016:40Professor Helmut Schwichtenberg, from the Ludwig Maximilians Universitaet Muenchen, Germany, visiting JAIST, will introduce his research on the computational content of proofs. The seminars will be as follows:
 Lecture 1. Computing with partial continuous functionals.
We define computable functionals of finite type, with the ScottErsov partial continuous functionals as domains. A term language T+ (a common extension of Goedel’s T and Plotkin’s PCF) is introduced to denote computable functionals.
 Lecture 2. A theory of computable functionals.
Based on T+ we define a logical language whose quantifiers range over partial continuous functionals and whose predicates are inductively defined. We obtain a theory TCF of computable functionals by adding introduction and elimination axioms for inductive predicates to minimal logic. TCF admits a realizability interpretation (by terms in T+) and a soundness theorem can be proved.
 Lecture 3. Extracting programs from proofs.
Every constructive proof of an existential theorem (or problem; Kolmogorov 1932) contains a construction of a solution. To get hold of such a solution we have two methods. (a) Writeandverify. Guided by the constructive proof directly write a program to compute the solution, and then prove (verify) that this is the case. (b) Proveandextract. Formalize the proof and extract its computational content in the form of a realizing term t. Since the latter approach requires formalization of the proof it is less popular. But it has advantages. (i) Dealing with a problem on the proof level allows abstract mathematical tools and a good organization of the material. Both help to adapt the proof to changed specifications. (ii) The extracted term can be automatically verified, by means of a formalization of the soundness theorem. As an example of the proveandextract method we build a parser for the Dyck language of balanced parentheses.
 Lecture 1. Computing with partial continuous functionals.

Departmental Seminar at the University of Canterbury, Christchurch: Towards a Rigorous Foundation for Bishop’s Constructive Analysis
(13 March 2014) 15:00Professor Giovanni Sambin, from the Università degli Studi di Padova, Italy, visiting Canterbury, will speak about the foundation of constructive analysis.

Ueber die Metamathematik kommutativer Ringe (d’apres Scarpellini)
(14 May 2014)Dr Peter Schuster, from the University of Leeds, UK, visiting LMU will give a talk about his contribution to the CORCON project.
Eine auf Krull zurueckgehende Variante des Zornschen Lemmas besagt, dasz ein Element eines kommutativen Ringes dann (und nur dann) nilpotent ist, wenn es in allen Primidealen liegt. Durch Interpolation einer von Scarpellini angegeben algebraischen Charakterisierung der Beweisbarkeit in kommutativen Ringen und Integritaetsringen können wir nun ein rein syntaktisches Gegenstueck zeigen: Die Theorie der Integritaetsringe ist bezueglich HornKlauseln eine konservative Erweiterung der Theorie der reduzierten Ringe, d.h. beide Theorien beweisen dieselben HornKlauseln.

JAIST: Pointfree foundations of Mathematics
(22 May 2014) 15:30Dr Marco Benini, from the Università degli Studi dell’Insubria, Italy, visiting JAIST will give a talk about his contribution to the CORCON project.
Is it possible to work with logical theories without assuming the existence of a universe where to interpret terms? This talk will positively answer to the above question in the case of firstorder, intuitionisticbased theories by providing a class of models, defined inside Category Theory, such that they allow to interpret theories in a sound and complete way. Furthermore, the models explain the computational meaning of the corresponding theories via a semantic version of the CurryHoward isomorphism. And their peculiar aspect is that they provide no universe where to interpret terms.

Analysis of Three Different Flavours. A story of examples, counterexamples, and viewpoints.
(28 May 2014)Dr Maarten McKubreJordens, from the University of Canterbury, New Zealand, visiting LMU, will give a talk about the CORCON project’s themes.
In this talk, which surveys at least two viewpoints both about and within mathematics, work is presented in three areas: (i) Constructive partial differential equations (“applied” constructive mathematics); (ii) Reverse constructive mathematics; (iii) Paraconsistent mathematics. A (very) brief introduction to Bishopstyle constructive mathematics will be given. In the first topic, we provide sufficient conditions for constructive existence of solutions to Dirichlettype problems, and outline where the classical existence proofs fail to be constructive. A corollary will be that there cannot be a universal algorithm that computes solutions to the NavierStokes equations of fluid flow. In the second topic, we show a direct proof of a known result: that compactness properties (of a certain kind) follow from a nonconstructive omniscience principle. The direct proof highlights the decision procedure that has to be made for those compactness properties. The third topic ventures into the littleknown realm of mathematics where contradictions may be allowed (yet sensible conclusions can still be drawn)and surprisingly find that proofs can be very constructive in that setting. As a hint at the riches that may be established paraconsistently, we take a look at compactness of closed bounded intervals in the real line.

Operators, singly, in bunches, and constructively
(4 June 2014)Professor Douglas Bridges, from the University of Canterbury, New Zealand, will speak about his research in the CORCON project.
I shall discuss a variety of results and conjectures in the constructive theory of operators and operator spaces. In particular, I shall consider how to locate the range of an operator between Banach spaces, how to locate the closure of Rx when R is a subspace of the space B(H) of bounded operators on a Hilbert space H and x in H, and how to characterise weakoperator continuous linear functionals on linear subsets of B(H). If time permits, I may also talk about relatively recent work with Ishihara and McKubreJordens, on reflexivity in Banach spaces.

Programming modulo representations
(5 June 2014)Dr Marco Benini, from Università degli Studi dell’Insubria, visiting JAIST, Japan, will talk about his research on programming in the typed lambdacalculus

BiIntuitionistic Modal Logic and Hypergraphs
(27 June 2014) 15:00Dr John Stell, from the University of Leeds, UK, will give a talk at JAIST about his contribution to the CORCON project.
I will discuss motivations from spatial reasoning and mathematical morphology (as used in image processing) for the notion of a relation on a graph. I will show how the algebra of these relations is weaker than that of relations on a set. This leads to a generalization of relation algebras in which the Boolean algebra is replaced by a symmetric Heyting algebra.
These relations can be used as the accessibility relations for a modal logic in which propositions are interpreted as subgraphs of a graph or more generally a hypergraph. 
Continuous Functions on NonWellfounded Types
(9 July 2014)Dr Dirk Pattinson, from the Australian National University, Australia, will introduce this joint work with Neil Ghani and Peter Hancock, which is part of the CORCON project.
The wellknown representation of real numbers as infinite streams of digits is a wellstudied instance of the use of coinductive types to represent continuous data types. The fact that also (total) continuous functions may be represented as a coinductive type suggests that this analogy can be carried over to a larger variety of structures and spaces usually found in analysis, with the main benefit of being able to use coinduction both as a definition and a proof principle on representatives. We argue that indeed many types of spaces found in analysis can be represented coinductively by generalising known representation theorems for function spaces from infinite streams to infinite trees, and subsequently to spaces of higherorder functions. The main challenge is to adequately capture the topology on the represented spaces, which leads to an informationtheoretic interpretation.

Programming Modulo Representations
(1 October 2014)Dr Marco Benini, from the University of Insubria, Italy, will speak in the Algebra, Logic, and Algorithms seminar at the University of Leeds.
The aim of this talk is to show, through an elementary example, how one can change the point of view on (functional) programming. The idea has a philosophical motivation: is it possible to conceive a programming system which does not allow to inspect its output and, at the same time, is able to ensure that the result of a computation is correct? This talk will provide a positive answer, but its consequences are still workinprogress.

An Algebraic Approach to Parametricity
(29 October 2014)Prof Neil Ghani, from the University of Strathclyde, UK, will speak in the Algebra, Logic, and Algorithms seminar at the University of Leeds.
The world is more uniform than we might imagine. For example it is riven with symmetries whose mathematical formalisation has proved to be of fundamental importance. These uniformities exist not just in Physics and Mathematics, but also in Logic and Computer Science. For example, polymorphic functions such as the function rev : List A > List A (which reverses every element of a list containing elements of type A) does not inspect the type A. Indeed, rev ignores the type A and rather performs an algorithm which does not vary as A varies. The algorithm for reversing a list of integers is exactly the same as that for reversing a list of strings! This phenomenon has come to be known in programming languages research as parametricity and is one of the most sophisticated tools possessed by programming language researchers.
I’d go further. I believe parametricity has much deeper significance than its incarnation within programming languages research might suggest. In order to deploy parametricity outside programming languages we need to develop a more abstract understanding of parametricity and in this talk I will sketch some ways in which I have been doing this. My fundamental conclusion is this: while our understanding of the world is usually inherently categorical (being built from the language of categories, functors and natural transformations) parametricity involves a fibrational understanding of the world based upon fibrations, fibred functors and fibred natural transformations. The aim of my talk will be to get the ideas behind this position across and thus I will not assume familiarity with either parametricity or category theory.