CCC is a workshop series that brings together researchers applying logical methods to the development of algorithms, with a particular focus on computation with infinite data, where issues of continuity, computability and constructivity play major roles. Specific topics include exact real number computation, computable analysis, effective descriptive set theory, constructive analysis, and related areas. The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and other continuous data, which are of increasing importance in safety critical applications and scientific computation.
CCC 2021 will be the 10th edition in the series. It will be organised by the School of Computer Science of the University of Birmingham but take place online.
(All times in UTC+1 (= English summer time))
| Monday morning session, chair Norbert Müller | ||
| 8:50 | Welcome | |
| 9:00 | Arno Pauly | Weihrauch degrees of problems related to topological circles |
| 9:30 | Pieter Collins | Rigorous Function Calculi-IV |
| 10:00 | Break | |
| 10:15 | Vittorio Cipriani and Arno Pauly | Embeddability of graphs and Weihrauch degrees |
| 10:45 | Anupam Das | A circular version of Gödel's T and its abstraction complexity |
| 11:15 | Nikolay Shilov, Dmitry Kondratyev and Boris Faifel | Platform-independent model of fix-point arithmetic for verification of the standard mathematical function |
| 11:45 | Lunch | |
| Monday afternoon session, chair Michal Konečný | ||
| 13:00 | Invited talk: Suguman Bansal | Towards designing intelligent machines via reactive synthesis |
| 14:00 | Tea | |
| Tuesday (Special session in honour of Ulrich Berger) chair Helmut Schwichtenberg | ||
| 9:00 | Invited talk: Monika Seisenberger | Advances in Program Extraction |
| 10:00 | Break | |
| 10:15 | Dieter Spreen and Ulrich Berger | Computing with Compact Sets: the Gray Code Case |
| 10:45 | Gianluca Curzi and Anupam Das | Towards Cyclic Implicit Complexity |
| 11:15 | Matthias Eberl | Continuity for Computability |
| 11:45 | Lunch | |
| Tuesday afternoon session, chair Daniel Graça | ||
| 13:00 | Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu | A Certified Library of Ordinal Arithmetic |
| 13:30 | Sewon Park, Holger Thies and Hideki Tsuiki | IFP style proofs in the Coq proof assistant |
| 14:00 | Tea | |
| Wednesday morning session, chair Alex Simpson | ||
| 9:00 | Invited talk: Franz Brauße | A δ-complete calculus for solving non-linear constraints |
| 10:00 | Break | |
| 10:15 | Takayuki Kihara | Lawvere-Tierney topologies for computability theorists |
| 10:45 | Michele Contente and Maria Emilia Maietti | Homotopy Type Theory as a logical framework for the Minimalist Foundation |
| 11:15 | Davide Trotta, Matteo Spadetto and Valeria de Paiva | Dialectica logical principles via free categorical constructions |
| 11:45 | Lunch | |
| Wednesday afternoon session, chair Milly Maietti | ||
| 13:00 | Tutorial: André Platzer | Programming and Proving with Dynamical Systems (Part 1) |
| 14:00 | Tea followed by CID Business Meeting | |
| Thursday morning session, chair Paul Potgieter | ||
| 9:00 | Invited talk: Sewon Park | Toward verified real computation |
| 10:00 | Break | |
| 10:15 | Peter Schuster and Daniel Wessel | Radical theory of Scott-open predicates |
| 10:45 | Willem Fouche | Logical and computational aspects of Gleason's theorem in probability theory |
| 11:15 | Michal Gajda | ULF -- Ultrafinitist and Ultraconstructivist Logical Framework |
| 11:45 | Lunch | |
| Thursday afternoon session, chair Monika Seisenberger | ||
| 13:00 | Tutorial: André Platzer | Programming and Proving with Dynamical Systems (Part 2) |
| 14:00 | Tea | |
| Friday morning session, chair Mathieu Hoyrup | ||
| 9:00 | Iosif Petrakis | From Daniell spaces to the integration spaces of Bishop and Cheng |
| 9:30 | Partha Pratim Ghosh | The Kuratowski Mrowka theorem for internal preneighbourhood spaces |
| 10:00 | Break | |
| 10:15 | Matthew de Brecht | Quasi-Polish spaces as spaces of ideals |
| 10:45 | Eike Neumann | On Envelopes and Backward Approximations |
| 11:15 | Jihoon Hyun, Hyunwoo Lee and Martin Ziegler | Computing the Mandelbrot Set, Reliably |
| 11:45 | Lunch | |
| Friday afternoon session, chair Pieter Collins | ||
| 13:00 | Invited talk: Michael Yampolsky | Towards understanding the theoretical challenges of numerical modeling of dynamical systems |
| 14:00 | Tea | |
Submission is now closed
Registration is free of charge. Simply email one of the organisers to receive information on how to join the Zoom sessions
Dieter Spreen and Achim Jung