We discuss the iterative solution of a finite element discretisation of the magma dynamics equations.  These equations share features of the Stokes equations, however, Elman-Silvester-Wathen (ESW) preconditioners for the magma dynamics equations are not optimal. By introducing a new field, the compaction pressure, into the magma dynamics equations, we have developed a new three-field preconditioner which is optimal in terms of problem size and less sensitive to physical parameters compared to the ESW preconditioners.

 Voevodsky asked what the topology of the universe is in a 
continuous interpretation of type theory, such as Johnstone's 
topological topos. We can actually give a model-independent answer: it 
is indiscrete. I will briefly introduce "intensional Martin-Loef type 
theory" (MLTT) and formulate and prove this in type theory (as opposed 
to as a meta-theorem about type theory). As an application or corollary, 
I will also deduce an analogue of Rice's Theorem for the universe: the 
universe (the large type of all small types) has no non-trivial 
extensional, decidable properties. Topologically this is the fact that 
it doesn't have any clopens other than the trivial ones.

It is well-known that a matrix $A$ is Hurwitz stable if and only if there exists a positive definite solution to the Lyapunov matrix equation $A X + X A^* = B$, where $B$ is Hermitian negative definite. We present a verified numerical algorithm to rigorously prove the stability of a given matrix $A$ in the presence of rounding errors.  The computational cost of the algorithm is cubic and it is fast since we can cast almost all operations in level 3 BLAS for which interval arithmetic can be implemented very efficiently.  This is a joint work with Andreas Frommer and the results are already published in ETNA in 2013.

Networks are a convenient way to represent systems of interacting entities. Many networks contain "communities" of nodes that are more densely connected to each other than to nodes in the rest of the network.

Most methods for detecting communities are designed for static networks. However, in many applications, entities and/or interactions between entities evolve in time.

We investigate "multilayer modularity maximization", a method for detecting communities in temporal networks. The main difference between this method and most previous methods for detecting communities in temporal networks is that communities identified in one temporal snapshot are not independent of connectivity patterns in other snapshots.  We show how the resulting partition reflects a trade-off between static community structure within snapshots and persistence of community structure between snapshots. As a focal example in our numerical experiments, we study time-dependent financial asset correlation networks.