We investigate the foundations of Choreographic Programming, a paradigm for writing concurrent programs that are deadlock free by construction, guided by the notion of computation. We start by introducing Minimal Choreographies (MC), a language that includes only the essential primitives of the paradigm. MC is minimal with respect to Turing completeness: it implements all computable functions, and restricting its syntax breaks this property. Our methodology yields a natural notion of computation for choreographies, which can be used to generate concurrent implementations of independent computations automatically. Finally, we show that a Turing complete fragment of MC can be correctly projected to a process calculus (synthesis), which is thus both deadlock free and Turing complete.

The Lorenz model was first studied by E. N. Lorenz and provides one of the first examples of a candidate of a strange attractor (the Lorenz attractor). The Lorenz attractor is rather difficult to study from a mathematical point of view, and its own existence was listed as one of the century problems by the Fields medalist Steve Smale. To make the analysis of the Lorenz model more amenable, a geometric model was introduced and it was recently shown in 2002 by Tucker that the Lorenz system behaves like the geometric model and hence has a strange attractor. In this talk we will analyze the geometric Lorenz model from a computability perspective and show that its associated strange attractor is computable, thus showing that the Lorenz attractor is also computable. We will also show that the Lorenz attractor has an associated computable measure.

In the movie “Life is Beautiful”, Guido Orefice, the character interpreted by Roberto Benigni, convinces his son Giosuè that they have been interned in a nazi concentration camp not because they are Jews but because they are actually taking part in a long and complex game in which they, and in particular Giosuè, must perform the tasks that the guards give them. A ghastly experience is turned into a livable, at times even almost enjoyable, one. We advocate that, in the same spirit as Guido’s ingenious trick of turning a nazi camp into a sort of playground for his child, security should be beautiful; and if it isn’t so yet, it should then be made beautiful, so that the users experience it in that way. This is, of course, an extremely challenging objective, and we will discuss through further scenarios a few ways in which it could be made possible in the future. It turns out that the Peppa Pig cartoon may also be inspiring.

What do variables in sequent calculus proof terms stand for? What is co-control and what is a co-continuation?  Answering these questions is required, if a full understanding of the Curry-Howard isomorphism for sequent calculus is to be achieved. This talk is about a recent answer to these questions, which led to the interpretation that sequent calculus is a formal vector notation (for lambda-terms) with first-class co-control.

In [1] we presented a logic for finitary epimorphisms which can be seen as an extension of Birkhoff's equational logic. In subsequent papers with Jiří Adámek and Michel Hébert, we obtained generalizations in several directions, in particular the Orthogonality Logic ([2,3]). After a first quick account of these results, I will present recent work with Jiří Adámek and Jiří Velebil on a generalization of this last logic in the setting of order-enriched categories.

1. J. Adámek, M. Sobral, L. Sousa, A logic of implications in algebra and coalgebra, Algebra Univers. 61 (2009) 313-337.
2. J. Adámek, M. Hébert, L. Sousa, A logic of orthogonality, Archivum Mathematicum 42, no.4, (2006), 309-334.
3. J. Adámek, M. Hébert, L. Sousa, The orthogonal subcategory problem and the small object argument, Appl. Categ. Structures 17 (2009), no. 3, 211-246.

In this talk, we present a number of examples in partial differential equations (PDE) where computer algebra and quantifier elimination methods can be used to prove theorems. These include systems of polynomial inequalities arising in PDE estimates and the construction of conserved and dissipated quantities for partial differential equations.

The transition from classical to quantum physics involves some choices related with the geometry of the phase space M. Contrary to what is frequently believed the resulting quantum theory does depend on these choices.

We will review an approach to study this dependence based on letting time, in Hamiltonian dynamics, become complex but still define evolution on M. This evolution does not only move points of M but also changes the (Kahler) geometry on the phase space along geodesics in the space of geometries.

Joint work with João P. Nunes.

After small considerations on the concept of machine and the paradoxes of its articulation with men’s life, I will do a short presentation of the main thesis of extended mind trying  to show how the leibnizianan theory of symbolism offers a fundamental basis for the contemporary theses about the continuity man-universal machine.