Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
By Marie Kerjean
Geometric Laplacians on Self-Conformal Fractal Curves in the Plane
By Naotaka Kajino
Appears in collection : Logic and transdiciplinarity: Mathematics/Computer Science/ Philosophy/Linguistics / La Logique et la transdisciplinarite : Maths/Info/Philo/Linguistique
In this programmatic talk, we will sketch both a conceptual and formal framework for reasoning about the notion of algorithm. This framework will arise from the analysis we will make of the relationships existing between the notion of algorithm and other similar (but still different) notions, like that of computation and that of program. We will first show that the Turing-Church thesis concerning effective computability is not sufficient to capture the notion of algorithm, as it identifies programs which are intensionally different. We will then show the limits of the existing models of computation in capturing some basic construction processes that we are willing to call algorithmic. In order to solve this problem, we propose a formalisation of the notion of model of computation on the base of which we claim that the notion of algorithm could eventually be analyzed. This approach centered around the dynamics of program execution, reconciles the more mechanical view of computation (such as formalized by Turing machines and automata) with the logical view - as it in particular stems from a generalization of Jean-Yves Girard's Geometry of Interaction programme.