13 February 2021 Abstracts of Contributed Papers

20 February 2021 Notification of Acceptance

27 February 2021 Early Registration: Reduced Fee

13 March 2021 Registration Closed

Correctness by Multiplication (CORCON) is an FP7 EU-funded project under the Marie Curie IRSES schema. This workshop aims at bringing together the participants and those researchers who are interested in the themes of the project.

The main themes of the project and the workshop are as follows:

- Proof Theory, Type Theory, and Constructive Set Theory Studying systems which are simultaneously able to compute and prove the correctness of computations means we need to study the interrelated areas of type theory, proof theory and constructive set theory. Type theory is an abstraction of a programming language where non-fundamental details are removed, proof theory is a technique which tells us what type theories can and can’t do, and constructive set theory allows us to ensure that when we prove something, no non-implementable aspects are used in the proof.
- Constructive Topology and Analysis Of particular sophistication is computation between real numbers and, more generally, infinitary structures. This necessitates the development of constructive versions of the standard branches of mathematics that deal with real numbers and the like, that is the development of constructive analysis and constructive topology.
- Homotopy Type Theory One of the major problems within correct by Multiplication programming is equality. We won’t have a proper understanding of the logic of computation until we can understand the logic of computing proofs that various computational entities are equal. The nature of equality was always been a major philosophical issue, but now, the need for a constructive and computational treatment of equality has become a fundamental problem inhibiting progress in a number of areas.
- Categorical Logic Logic has always been greatly influenced by its model theory which has a more algebraic flavour and this is no different for the sorts of logics needed by correct by Multiplication programming. Of particular relevance is category theory which has been shown to be a powerful tool for understanding logical theories. Within this framework, our understanding of the logics needed for correct by Multiplication programming will be enhanced by developing their categorical semantics.
- Programming Languages for Correct by Multiplication Programming Of course, once we have clean logical abstractions capable of supporting correct by Multiplication programming, we need to actually turn them into the programming languages, idioms, and abstractions of the future.
- Correct by Multiplication programs over continuous data Similarly, we require dedicated programming languages, idioms and abstractions tailored to correct by Multiplication programs which manipulate continuous data.
- Correct by Multiplication Programs with Limited Resources And finally, as computation becomes ever more localised and autonomous, we need to understand how all of the above can be executed in a low resourced environment.

The workshop is also kindly sponsored by AILA (Associazione Italiana di Logica e sue Applicazioni), IC-EATCS (Italian Chapter of the European Association for Theoretical Computer Science) and the Italian national research project Logical Methods of Information Management.

Downloadable programme (pdf) : tables-de-multiplication.com

08.00 Building opens

09.00-09.30 Registration and Opening

09.30-10.15 Giovanni Sambin, On the so-called axiom of unique choice

10.15-10.45 Coffee break

10.45-11.30 Maria Emilia Maietti, Computation by Multiplication in the Minimalist Foundation

11.30-12.15 Helmut Schwichtenberg, Realizability

12.15-14.30 Lunch break

14.30-15.15 Iosif Petrakis, Limit spaces with approximations

15.15-16.00 Monika Seisenberger, Program extraction with infinite data

16.00-16.30 Coffee break

16.30-17.15 Mizuhito Ogawa, Satisfiability of arithmetic constraints and its applications on verification

19.00 Building closes

08.45-09.30 Satoshi Tojo, Who knows what at which time? – from viewpoint of dynamic epistemic logic

09.30-10.15 Hideki Tsuiki, Dyadic subbases derived from dynamical systems

10.15-10.45 Coffee break

10.45-11.30 Katsuhiko Sano, Topological semantics for Visser’s propositional logics

11.30-12.15 Gianluigi Bellin and Alessandro Menti, Bi-intuitionism as dialogue chirality

12.15-14.30 Lunch break

14.30-15.15 Gyesik Lee, The big five systems of reverse mathematics and their computational interpretation

15.15-16.00 Keita Yokoyama, The strength of Ramsey’s theorem from several different view points

16.00-16.30 Coffee break

16.30-17.15 Sam Sanders, Higher-order reverse mathematics of Brouwer’s continuity theorem and related principles

17.15-18.15 CORCON General Project Meeting

08.45-09.30 Neil Ghani, Parametricity – what’s it all about

09.30-10.15 Michael Rathjen, Indefiniteness of mathematical problems?

10.15-10.45 Coffee break

10.45-11.30 Takako Nemoto, Interpretation of set theory into theory of operators

11.30-12.15 Takayuki Kihara, Arboreal forcings over admissible sets

12.15-14.30 Lunch break

14.30-15.15 Hajime Ishihara, A monad in the combinatory algebras

15.15-16.00 Francesco Ciraulo, Positivity relations and localic suplattices

16.00-16.30 Coffee break

16.30-17.15 Dieter Spreen, Information frames and L-domains

17.15-18.15 CORCON Work Packages Meetings (20 min for each WP)

Relating Core Logical Systems

Topology and Analysis; Reverse Mathematics

Types and Categories; Programming Languages

20.00 Conference Dinner

08.45-09.30 Hannes Diener, BD-N

09.30-10.15 Tatsuji Kawai, Point-free characterisation of Bishop compact metric spaces

10.15-10.45 Coffee break

10.45-11.30 Olaf Beyersdorff, How difficult is it to verify proofs?

11.30-12.15 Marco Benini, Does programming really need data structures?

12.15-14.30 Lunch break

14.30-15.15 Eugenio Moggi, Categories for collection types

15.15-16.00 Giuseppe Rosolini, Frames as equilogical spaces

Please register as soon as possible, in any case before 14 March 2021, by sending a message to corcon-ge@googlegroups.com with Subject your “Name-Surname” and the following information

Title (e.g. Mr, Mrs, Prof,…)

Name

Surname

Affiliation

Country

Email (if different from the one used for sending the message)

URL of you web page (optional)

Expected Date of Arrival (optional)

Expected Date of Departure (optional)

Additional Information (optional, e.g. dietary restrictions)

If you cannot attach to the message a receipt (in pdf format) of the bank transfer for the payment of the registration fee, you should send a second message, with the same subject, as soon as you have the receipt (see below for further details).

The fee include only coffee breaks (lunches and dinner are not included)

100€ to be paid before 14 March 2021. Before the same date, a copy of the receipt of payment must be sent to the e-address corcon-ge@googlegroups.com OR faxed to +390103536699.

60€ for participants who send the copy of the receipt of payment before Friday, 28 February 2021.

The registration must be paid by bank transfer to

UNIVERSITA’ DEGLI STUDI DI GENOVA Dipartimento di Matematica – DIMA via Dodecaneso 35 16146 Genova

IBAN: IT11B0617501472000000534690

BIC/SWIFT: CRGEITGG090

The bank details, in case they are needed, are

BANCA CARIGE S.p.A. Agenzia 41 – Via G. D’Annunzio 39 16121 GENOVA

Please make sure to specify that the reason for payment is DIMA – CORCON2021 – “write your surname here” Make sure to check the list of participants to see if your details have been received correctly. In case the fees that your bank charges for the order are very high, please check with us if on-site payment is possible.

List of participants ordered by Surname

Name | Surname | Affiliation | Country |
---|---|---|---|

Gianluigi | Bellin | Univ. of Verona | Italy |

Marco | Benini | Univ. of Insubria | Italy |

Olaf | Beyersdorff | Univ. of Leeds | United Kingdom |

Francesco | Ciraulo | Univ. of Padua | Italy |

Hannes | Diener | Univ. of Siegen | Germany |

Jacopo | Emmenegger | Univ. of Siena | Italy |

Neil | Ghani | Univ. of Strathclyde | United Kingdom |

Enrico | Ghiorzi | Univ. of Cambridge | United Kingdom |

Stefano | Gogioso | Univ. of Oxford | United Kingdom |

Hajime | Ishihara | JAIST | Japan |

Tatsuji | Kawai | JAIST | Japan |

Takayuki | Kihara | JAIST | Japan |

SunYoung | Kim | Yonsei University | South Korea |

Gyesik | Lee | Hankyong National University | South Korea |

Junguk | Lee | Yonsei University | South Korea |

Maria Emilia | Maietti | Univ. of Padua | Italy |

Samuele | Maschio | Univ. of Padua | Italy |

Alessandro | Menti | Univ. of Verona | Italy |

Eugenio | Moggi | Univ. of Genoa | Italy |

Takako | Nemoto | JAIST | Japan |

Mizuhito | Ogawa | JAIST | Japan |

Ruggero | Pagnan | Univ. of Genoa | Italy |

Erik | Palmgren | Stockholm University | Sweden |

Iosif | Petrakis | Univ. of Munich | Germany |

Michael | Rathjen | Univ. of Leeds | United Kingdom |

Giuseppe | Rosolini | Univ. of Genoa | Italy |

Giovanni | Sambin | Univ. of Padua | Italy |

Sam | Sanders | Ghent University | Belgium |

Katsuhiko | Sano | JAIST | Japan |

Peter | Schuster | Univ. of Leeds | United Kingdom |

Helmut | Schwichtenberg | LMU Munich | Germany |

Monika | Seisenberger | Swansea University | United Kingdom |

Dieter | Spreen | Univ. of Siegen | Germany |

John | Stell | Univ. of Leeds | United Kingdom |

Kazuyuki | Tanaka | Tohoku University | Japan |

Satoshi | Tojo | JAIST | Japan |

Hideki | Tsuiki | Kyoto University | Japan |

Keita | Yokoyama | JAIST | Japan |

Keisuke | Yoshii | Tohoku University | Japan |

DIMA, via Dodecaneso 35, 16146 Genova. All sessions take place in room 704 on the 7th floor (the main entrance is located on the 6th floor). Internet access is available via eduroam in most parts of the building.

The Department of Mathematics (DIMA) is at via Dodecaneso 35, 16146 Genova, in the area called Valletta Puggia not far from corso Europa which is the main road which runs through the eastern part of Genoa, from the town centre to Nervi. The Department is open on weekdays, from 8am to 7pm.

The hotels which offer special accommodation to visitors of the University are the following:

Hotel | * | address | area | single | double |
---|---|---|---|---|---|

Capannina | 3 | via Speri 7 | Albaro | €55.00 | €75.00 |

Il Giardino di Albaro | 3 | via De Gaspari 19 | Albaro | €89.00 | €110.00 |

Brignole | 3 | vico Corallo 22 | Brignole | €57.00 | €67.00 |

Astoria | 3 | piazza Brignole 4 | Brignole | €80.00 | €105.00 |

Starhotel President | 4 | corte Lambruschini 4 | Brignole | €90.00 | €110.00 |

Moderno Verdi | 4 | piazza Verdi 5 | Brignole | €90.00 | €125.00 |

The Department of Mathematics is in the area called Albaro. It can be reached on foot in 25-30 minutes from the hotels in that area; it can be reached by bus (and a short climb) in 15-20 minutes from Brignole.

There are regular buses from the main stations Brignole and Principe. We strongly recommend, if possible, to get off the train at Brignole.

Outside Stazione Brignole, buses which go to Corso Gastaldi are 16, 17, 45, 85, 86 ,87. All stop at the platform marked Bus: levante away from the station. You have to get off bus 17 near Ospedale San Martino. It is easy to recognize when you are on corso Gastaldi because it is a very large road which climbs up and has railroad tracks on its left. It ends just after the tracks disappear. At that point you may ring the bell to request the bus stops. On the right you may notice the following big signs in succession: “COOP” in red, “OPEL” in yellow. Walk back along the road for some 50 meters, then on your left take the steps of Salita Papigliano. Cross the first road you meet (Via San Martino). Climb up along Via Papigliano, to reach Via Padre Semeria, a small lane enclosed by high walls. You see a small gate in front of you: go through it and walk the metal bridge. When you are to take the steps down, you see the main entrance to DIMA, the Departments of Mathematics. However if you are on bus 45, 85, 86, or 87, note that the bus leaves Corso Gastaldi and enters Via San Martino. You should get off at the second stop on Via San Martino (when crossing via Papigliano). Then follow the instructions above.

From Stazione Principe, take a train to Genova Brignole (a bus ticket allows to ride trains within the town) and then take a bus (see instructions above). By train, it takes about 10 minutes to go from Principe to Brignole.

From the centre of town (Piazza De Ferrari), take bus 44 from Via Dante. After some 15 minutes, the route climbs a hill and the bus rides a bus lane in the middle of the road: it is Corso Gastaldi. Now follow the instructions above.

You can buy bus tickets at tobacconists’, newagents’, at ticket counters outside the main train stations. A ticket is valid for 100 mins. on buses, metro, and trains in the metropolitan area, e.g. from Principe to Brignole.

There are many fast trains from Milano Centrale to Genova Principe (some of these continue to Brignole), approximately one every hour. An InterCity train leaves every other hour from 9.10 to 19.10. There are also many fast trains from Pisa Centrale to Brignole as well as from Torino Porta Nuova.

If you arrive by car at Genoa on one of the motorways, you should take the exit of Genova Nervi, on motorway A12, Genova-Livorno. If you are on another motorway, follow the directions for A12 Livorno. From the exit follow the directions for CENTRO. They will take you very soon on Corso Europa. You must turn left on via Corridoni, the first allowed left turn on corso Gastaldi which just continues corso Europa after passing Ospedale San Martino. You may spot a sign on the left directing to the Facoltà di Ingegneria. After a few bends, the road becomes via Monte Zovetto, then via Perosio, and enters piazza Leonardo da Vinci. Turn left in the square, pass the first traffic light and get into via Boselli, left again at the next traffic light, and left once more into via Pisa. Finally take the second right into via Flora, this continues into via Dodecaneso. The entrance to the site is after the street narrows, and DIMA is at the far end of the building.

The line Volabus is the fast bus between the airport “C. Colombo” and the centre. The ticket costs 6€ and one can ride on any other bus with it for another hour. From the airport, Volabus reaches Stazione Piazza Principe (often erroneously called Porta Principe), the central Piazza De Ferrari, and Stazione Brignole. A taxi ride from the airport to the area near DIMA is about 28€.

Abstracts in PDF, at most one page including references, can only be

submitted via EasyChair.

In addition to contributions from members of the project sites, there

will also be room for a few contributions by people from outside the

project.

13 February 2021 Abstracts of Contributed Papers

20 February 2021 Notification of Acceptance

27 February 2021 Early Registration: Reduced Fee

13 March 2021 Registration Closed

- Marco Benini (Insubria, Italy)
- Neil Ghani (Strathclyde, UK)
- Hajime Ishihara (JAIST, Japan)
- Gyesik Lee (HNU, Korea)
- Maria Emilia Maietti (Padua, Italy)
- Eugenio Moggi (Genoa, Italy)
- Mizuhito Ogawa (JAIST, Japan)
- Erik Palmgren (Stockholm, Sweden)
- Michael Rathjen (Leeds, UK)
- Giuseppe Rosolini (Genoa, Italy)
- Giovanni Sambin (Padua, Italy)
- Helmut Schwichtenberg (Munich, Germany)
- Monika Seisenberger (Swansea, UK)
- Dieter Spreen (Siegen, Germany)
- John Stell (Leeds, UK)
- Satoshi Tojo (JAIST, Japan)
- Hideki Tsuiki (Kyoto, Japan)

Organisers (alphabetical order):

- Marco Benini (Insubria)
- Hannes Diener (Siegen)
- Neil Ghani (Strathclyde)
- Eugenio Moggi (Genova)
- Ruggero Pagnan (Genova)
- Giuseppe Rosolini (Genova)
- Peter Schuster (Leeds)
- Monika Seisenberger (Swansea)
- Dieter Spreen (Siegen)