Conference in honour of

Amílcar Sernadas

Instituto Superior Técnico,

Lisbon, Portugal.

April 23, 2016.

Conference in honour of

Amílcar Sernadas

Instituto Superior Técnico,

Lisbon, Portugal.

April 23, 2016.

- Olga Pombo, Faculdade de Ciências, Universidade de Lisboa
## Leibnizian grounds for the idea of universal machine

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.- José Mourão, CAMGSD, Instituto Superior Técnico
## Complex time evolution in geometry and in quantum physics

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.

- Diogo Gomes, King Abdullah University of Science and Technology
## Applied logic and computer algebra in partial differential equations

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.

- Lurdes Sousa, Instituto Politécnico de Viseu, Centro de Matemática da Universidade de Coimbra
## From Birkhoff's equational logic to Kan-injectivity logic

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.

- J. Adámek, M. Sobral, L. Sousa, A logic of implications in algebra and coalgebra, Algebra Univers. 61 (2009) 313-337.
- J. Adámek, M. Hébert, L. Sousa, A logic of orthogonality, Archivum Mathematicum 42, no.4, (2006), 309-334.
- 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.

- José Espírito Santo, Centro de Matemática, Universidade do Minho
## Curry-Howard for sequent calculus at last

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.

- José Fiadeiro, Royal Holloway, University of London
## Actor networks: a modelling framework for cyberphysical system protocols

Abstract: We outline actor networks as a formal model of computation in heterogenous networks of computers, humans and their devices. The formalism builds on Latour’s Actor Network paradigm, which has been very influential in sociology, emphasizing and analyzing the ways in which the interactions between people and objects, as equal factors, drive social processes. It also builds on other network-based models of computation that have become popular across sciences, from physics and biology, to sociology and computer science. This is joint work with Antónia Lopes (University of Lisbon) and Dusko Pavlovic (University of Hawaii).- Luca Viganò, King’s College London
## Security is beautiful

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.

- Fernando Ferreira, Faculdade de Ciências, Universidade de Lisboa
## Arithmetic and geometry from the formal point of view: some notes, some lessons

First-order Peano arithmetic and Tarski’s elementary geometry are quite different formal theories. The first one is incomplete and (essentially) undecidable whereas the second is complete and decidable. In this talk we point to other less well known properties and distinctions concerning formal theories of arithmetic and geometry. We will specially look at Raphael Robinson’s theory of arithmetic Q, a very weak theory without induction. Work due to Nelson, Solovay, Hajek, Buss, Wilkie, Paris, Pudlak, Visser, Friedman, Ferreira, etc. shows that there are very interesting theories which Robinson's Q is able to interpret. For instance, Q is able to interpret Tarski’s elementary geometry. In order to discuss this, we make a detour through weak analysis and the work of A. Fernandes, F. Ferreira and G. Ferreira.- Daniel Graça, Universidade do Algarve
## Computability of the Lorenz attractor

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.

- Luís Cruz-Filipe, University of Southern Denmark
## A Minimal Turing-Complete Choreography Calculus

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.