Correctness by Multiplication CORCON Workshop
24-27 2021 March, Genoa, Italy
Important deadlines
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
Info
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.
Themes
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.
Further info
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.
Programme
Downloadable programme (pdf) : tables-de-multiplication.com
24 March 2021
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
25 March 2021
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
26 March 2021
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
27 March 2021
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
Registration
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).
Fees
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.
Payment
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.
Participants
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 |
Venue
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.
Accommodation
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.
Buses
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.
Arriving by train
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.
Arriving by car
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.
Arriving by plane
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€.
Call for Papers
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.
Important Deadlines
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
Keynote Speakers
- 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)
Contacts
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)