Luigi Santocanale, publications 
My publication on DBLP (not all of them).
Manuscripts submitted
[1] 
S. Ghilardi, L. Santocanale, Ruitenburg's theorem via duality and bounded
bisimulations, submitted to the conference Advances in Modal Logic 2018.
(Mar. 2018).
[ Hal 
http ]
Abstract.
For a given intuitionistic propositional formula A
and a propositional variable x occurring in it,
define the infinite sequence of formulae { A_i 
i≥1} by letting A_1 be A and A_i+1 be
A(A_i/x). Ruitenburg's Theorem says that the
sequence { A_i } (modulo logical equivalence) is
ultimately periodic with period 2, i.e. there is N ≥
0 such that A_{N+2} ↔ A_N is provable in
intuitionistic propositional calculus. We give a
semantic proof of this theorem, using duality
techniques and bounded bisimulations ranks.

[2] 
M. J. Gouveia, L. Santocanale, Aleph1 and the Modal muCalculus, extended
version of the CSL 2017 conference paper. Submitted to Logical Methods in
Computer Science (Mar. 2018).
[ Hal 
http ]
Abstract.
For a regular cardinal κ, a formula of the
modal μcalculus is κcontinuous in a
variable x if, on every model, its interpretation
as a unary function of x is monotone and preserves
unions of κdirected sets. We define the
fragment C_{aleph_1}(x) of the modal
μcalculus and prove that all the formulas in
this fragment are aleph_{1}continuous. For each
formula φ(x) of the modal μcalculus, we
construct a formula ψ(x) C_{aleph_1}(x) such
that φ(x) is κcontinuous, for some
κ, if and only if φ(x) is equivalent to
ψ(x). Consequently, we prove that (i) the
problem whether a formula is κcontinuous for
some κ is decidable, (ii) up to equivalence,
there are only two fragments determined by
continuity at some regular cardinal: the fragment
C_{aleph_0}(x) studied by Fontaine and the
fragment C_{aleph_1}(x). We apply our
considerations to the problem of characterizing
closure ordinals of formulas of the modal
μcalculus. An ordinal α is the closure
ordinal of a formula φ(x) if its interpretation
on every model converges to its least fixedpoint in
at most α steps and if there is a model where
the convergence occurs exactly in α steps. We
prove that ω_{1}, the least uncountable
ordinal, is such a closure ordinal. Moreover we
prove that closure ordinals are closed under ordinal
sum. Thus, any formal expression built from 0, 1,
ω, ω_{1} by using the binary operator
symbol + gives rise to a closure ordinal.

[3] 
S. Ghilardi, M. J. Gouveia, L. Santocanale, Fixedpoint elimination in the
intuitionistic propositional calculus, extended version of the FOSSACS 2016
paper. Submitted to TOCL. (Feb. 2018).
[ Hal 
http ]
Abstract.
It is a consequence of existing literature that
least and greatest fixedpoints of monotone
polynomials on Heyting algebrasthat is, the
algebraic models of the Intuitionistic Propositional
Calculusalways exist, even when these algebras are
not complete as lattices. The reason is that these
extremal fixedpoints are definable by formulas of
the IPC. Consequently, the μcalculus based on
intuitionistic logic is trivial, every μformula
being equivalent to a fixedpoint free formula. We
give in this paper an axiomatization of least and
greatest fixedpoints of formulas, and an algorithm
to compute a fixedpoint free formula equivalent to
a given μformula. The axiomatization of the
greatest fixedpoint is simple. The axiomatization
of the least fixedpoint is more complex, in
particular every monotone formula converges to its
least fixedpoint by Kleene's iteration in a finite
number of steps, but there is no uniform upper bound
on the number of iterations. We extract, out of the
algorithm, upper bounds for such n, depending on the
size of the formula. For some formulas, we show that
these upper bounds are polynomial and optimal.

[4] 
L. Santocanale, F. Wehrung, The equational theory of the weak order on finite
symmetric groups, submitted to the Journal of the European Mathematical
Society (May 2014).
[ Hal 
http ]
Abstract.
It is wellknown that the weak Bruhat order on the
symmetric group on a finite number n of letters is a
lattice, denoted by P(n) and often called the
permutohedron on n letters, of which the Tamari
lattice A(n) is a lattice retract. The equational
theory of a class of lattices is the set of all
lattice identities satisfied by all members of that
class. We know from earlier work that the equational
theory of all P(n) is properly contained in the one
of all A(n). We prove the following
results. TheoremA. The equational theory of all P(n)
and the one of all A(n) are both decidable. Theorem
B. There exists a lattice identity that holds in all
P(n), but that fails in a certain 3338element
lattice. TheoremC. The equational theory of all
extended permutohedra, on arbitrary (possibly
infinite) posets, is trivial. In order to prove
Theorems A and B, we reduce the satisfaction of a
given lattice identity in a Cambrian lattice of type
A to a certain tiling problem on a finite
chain. Theorem A then follows from Büchi's
decidability theorem for the monadic secondorder
theory MSO of the successor function on the natural
numbers. It can be extended to any class of Cambrian
lattices of type A with MSOdefinable set of
orientations.

Articles in journals
[1] 
L. Santocanale, Embeddability into relational lattices is undecidable, Journal
of Logical and Algebraic Methods in Programming 97 (2018) 131148.
[ EE 
Hal ]
Abstract.
The natural join and the inner union operations
combine relations in a database. Tropashko and
Spight realized that these two operations are the
meet and join operations in a class of lattices,
known by now as the relational lattices. They
proposed then lattice theory as an algebraic
approach, alternative to the relational algebra, to
the theory of databases. Litak et al. proposed an
axiomatization in the signature extending the pure
lattice signature with the header constant. They
argued then that the quasiequational theory of
relational lattices is undecidable in this extended
signature. We refine this result by showing that the
quasiequational theory of relational lattices in the
pure lattice signature is undecidable as well. We
obtain this result as a consequence of the following
statement: it is undecidable whether a finite
subdirectlyirreducible lattice can be embedded into
a relational lattice. Our proof of this statement is
a reduction from a similar problem for relation
algebras and from the coverability problem of a
frame by a universal product frame. As corollaries,
we also obtain the following results: the
quasiequational theory of relational lattices has no
finite base; there is a quasiequation which holds in
all the finite lattices but fails in an infinite
relational lattice.

[2] 
S. Frittella, A. Palmigiano, L. Santocanale, Dual characterizations for finite
lattices via correspondence theory for monotone modal logic, Journal of Logic
and Computation 27 (3) (2017) 639678.
[ EE 
Hal ]
Abstract.
We establish a formal connection between algorithmic
correspondence theory and certain dual
characterization results for finite lattices,
similar to Nation's characterization of a hierarchy
of pseudovarieties of finite lattices, progressively
generalizing finite distributive lattices. This
formal connection is mediated through monotone modal
logic. Indeed, we adapt the correspondence algorithm
ALBA to the setting of monotone modal logic, and we
use a certain dualityinduced encoding of finite
lattices as monotone neighbourhood frames to
translate lattice terms into formulas in monotone
modal logic.

[3] 
L. Santocanale, F. Wehrung, Lattices of regular closed subsets of closure
spaces, International Journal of Algebra and Computation 24 (7) (2014)
9691030, 51 pages.
[ EE 
Hal ]
Abstract.
For a closure space (P,f), the closures of open
subsets of P, called the regular closed subsets,
form an ortholattice Reg(P,f), extending the poset
Clop(P,f) of all clopen subsets. If (P,f) is a
finite convex geometry, then Reg(P,f) is
pseudocomplemented. The DedekindMacNeille
completion of the poset of regions of any central
hyperplane arrangement can be obtained in this way,
hence it is pseudocomplemented. The lattice
Reg(P,f) carries a particularly interesting
structure for special types of convex geometries,
that we call closure spaces of semilattice type. For
finite such closure spaces, (1) Reg(P,f) satisfies
an infinite collection of stronger and stronger
quasiidentities, weaker than both meet and
joinsemidistributivity. Nevertheless it may fail
semidistributivity. (2) If Reg(P,f) is
semidistributive, then it is a bounded homomorphic
image of a free lattice. (3) Clop(P,f) is a
lattice iff every regular closed set is clopen. The
extended permutohedron R(G) on a graph G, and
the extended permutohedron Reg(S) on a
joinsemilattice S, are both defined as lattices
of regular closed sets of suitable closure
spaces. While the lattice of regular closed sets is,
in the semilattice context, always the Dedekind
MacNeille completion of the poset of clopen sets,
this does not always hold in the graph context,
although it always does so for finite block graphs
and for cycles. Furthermore, both R(G) and
Reg(S) are bounded homomorphic images of free
lattices.

[4] 
L. Santocanale, F. Wehrung, The extended permutohedron on a transitive binary
relation, European Journal of Combinatorics 42 (2014) 179206, 25 pages.
[ EE 
Hal ]
Abstract.
For a given transitive binary relation e on a set
E, the transitive closures of open (i.e.,
cotransitive in e) sets, called the regular
closed subsets, form an ortholattice Reg(e), the
extended permutohedron on e. This construction,
which contains the poset Clop(e) of all clopen
sets, is a common generalization of known notions
such as the generalized permutohedron on a partially
ordered set on the one hand, and the bipartition
lattice on a set on the other hand. We obtain a
precise description of the completely
joinirreducible (resp., completely
meetirreducible) elements of Reg(e) and the arrow
relations between them. In particular, we prove that
(1) Reg(e) is the DedekindMacNeille completion of
the poset Clop(e); (2) Every open subset of e is
a settheoretic union of completely joinirreducible
clopen subsets of e; (3) Clop(e) is a lattice
iff every regular closed subset of e is clopen,
iff e contains no ”square” configuration, iff
Reg(e)=Clop(e); (4) If e is finite, then
Reg(e) is pseudocomplemented iff it is
semidistributive, iff it is a bounded homomorphic
image of a free lattice, iff e is a disjoint sum
of antisymmetric transitive relations and
twoelement full relations. We illustrate the
strength of our results by proving that, for n
greater than or equal to 3, the congruence lattice
of the lattice Bip(n) of all bipartitions of an
nelement set is obtained by adding a new top
element to a Boolean lattice with n2^{n1}
atoms. We also determine the factors of the minimal
subdirect decomposition of Bip(n).

[5] 
L. Santocanale, F. Wehrung, Sublattices of associahedra and permutohedra,
Advances in Applied Mathematics 51 (3) (2013) 419445.
[ EE 
Hal ]
Abstract.
Grätzer asked in 1971 for a characterization of
sublattices of Tamari lattices. A natural candidate
was coined by McKenzie in 1972 with the notion of a
bounded homomorphic image of a free latticein
short, bounded lattice. Urquhart proved in 1978 that
every Tamari lattice is bounded (thus so are its
sublattices). Geyer conjectured in 1994 that every
finite bounded lattice embeds into some Tamari
lattice. We disprove Geyer's conjecture, by
introducing an infinite collection of
latticetheoretical identities that hold in every
Tamari lattice, but not in every finite bounded
lattice. Among those finite counterexamples, there
are the permutohedron on four letters P(4), and in
fact two of its subdirectly irreducible retracts,
which are Cambrian lattices of type A. For natural
numbers m and n, we denote by B(m,n) the
(bounded) lattice obtained by doubling a join of m
atoms in an (m + n)atom Boolean lattice. We prove
that B(m,n) embeds into a Tamari lattice iff min
m , n <=1, and that B(m,n) embeds into a
permutohedron iff min m , n <=2. In
particular, B(3,3) cannot be embedded into any
permutohedron. Nevertheless we prove that B(3,3)
is a homomorphic image of a sublattice of the
permutohedron on 12 letters.

[6] 
L. Santocanale, F. Wehrung, Varieties of lattices with geometric descriptions,
Order 30 (2013) 1338.
[ EE 
Hal ]
Abstract.
A lattice L is spatial if every element of L is a
join of completely joinirreducible elements of L (
points ), and strongly spatial if it is spatial and
the minimal coverings of completely joinirreducible
elements are wellbehaved. Herrmann et al. proved in
1994 that every modular lattice can be embedded,
within its variety, into an algebraic and spatial
lattice. We extend this result to n distributive
lattices, for fixed n . We deduce that the variety
of all n distributive lattices is generated by its
finite members, thus it has a decidable word problem
for free lattices. This solves two problems stated
by Huhn in 1985. We prove that every modular (resp.,
n distributive) lattice embeds within its variety
into some strongly spatial lattice. Every lattice
which is either algebraic modular spatial or
bialgebraic is strongly spatial. We also construct
a lattice that cannot be embedded, within its
variety, into any algebraic and spatial
lattice. This lattice has a least and a largest
element, and it generates a locally finite variety
of joinsemidistributive lattices.

[7] 
L. Santocanale, Y. Venema, Completeness for flat modal fixpoint logics, Annals
of Pure and Applied Logic 162 (1) (2010) 5582.
[ EE 
Hal ]
Abstract.
This paper exhibits a general and uniform method to
prove completeness for certain modal fixpoint
logics. Given a set Γ of modal formulas of
the form γ(x,p_{1},...,p_{n}), where x
occurs only positively in γ, the language
L_{#}(Γ) is obtained by adding to
the language of polymodal logic a connective
#_{γ} for each γinΓ. The term
#_{γ}(φ_{1},...,φ_{n}) is meant to
be interpreted as the least fixed point of the
functional interpretation of the term
γ(x,φ_{1},...,φ_{n}). We consider
the following problem: given Γ, construct an
axiom system which is sound and complete with
respect to the concrete interpretation of the
language L_{#}(Γ) on Kripke
frames. We prove two results that solve this
problem. First, let K_{#}(Γ) be
the logic obtained from the basic polymodal
by adding a KozenPark style fixpoint axiom and a
least fixpoint rule, for each fixpoint connective
#_{γ}. Provided that each indexing formula
γ satisfies the syntactic criterion of being
untied in x, we prove this axiom system to be
complete. Second, addressing the general case, we
prove the soundness and completeness of an extension
K^{+}_{#}(Γ) of
K_{#}(Γ). This extension is
obtained via an effective procedure that, given an
indexing formula γ as input, returns a finite
set of axioms and derivation rules for
#_{γ}, of size bounded by the length of
γ. Thus the axiom system
K^{+}_{#}(Γ) is finite whenever
Γ is finite.

[8] 
L. Santocanale, A nice labelling for treelike event structures of degree 3,
Information and Computation 208 (3) (2010) 652665, a special issue
dedicated to the conference CONCUR 2007.
[ EE 
Hal ]
Abstract.
We address the problem of finding nice labellings
for event structures of degree 3. We develop a
minimum theory by which we prove that the labelling
number of an event structure of degree 3 is bounded
by a linear function of the height. The main theorem
we present in this paper states that event
structures of degree 3 whose causality order is a
tree have a nice labelling with 3 colors. Finally,
we exemplify how to use this theorem to construct
upper bounds for the labelling number of other event
structures of degree 3.

[9] 
W. Belkhir, L. Santocanale, The variable hierarchy for the games
μcalculus, Annals of Pure and Applied Logic 161 (5) (2010) 690707.
[ EE 
Hal ]
Abstract.
Parity games are combinatorial representations of
closed Boolean μterms. By adding to them draw
positions, they have been organized by Arnold and
one of the authors into a μcalculus. As done by
Berwanger et al. for the propositional modal
μcalculus, it is possible to classify parity
games into levels of hierarchy according to the
number of fixedpoint variables. We ask whether this
hierarchy collapses w.r.t. the standard
interpretation of the games μcalculus into the
class of all complete lattices. We answer this
question negatively by providing, for each n >=
1, a parity game G_{n} with these properties: it
unravels to a μterm built up with n
fixedpoint variables, it is semantically equivalent
to no game with strictly less than n2 fixedpoint
variables.

[10] 
L. Santocanale, Topological properties of event structures, Electronic Notes in
Theoretical Computer Science 230 (2009) 149160, GETCO 2006, Geometrical
and Topological Methods in Concurrency, Bonn, August 26 2006.
[ EE 
.pdf ]
Abstract.
Motivated by the nice labeling problem for event
structures, we study the topological properties of
the associated graphs. For each n >=0, we
exhibit a graph G_{n} that cannot occur on an
antichain as a subgraph of the graph of an event
structure of degree n. The clique complexes of the
graphs G_{n} are disks (n even) and spheres (n
odd) in increasing dimensions. We strengthen the
result for event structure of degree 3: cycles of
length greater than 3 do not occur on antichains
as subgraphs. This amount to saying that the clique
complex of the graph of an event structure of degree
3 is acyclic.

[11] 
L. Santocanale, Derived semidistributive lattices, Algebra Universalis 63 (2)
(2010) 101130.
[ EE 
Hal ]
Abstract.
For L a finite lattice, let C(L)
denote the set of pairs γ=
(γ_{0},γ_{1}) such that γ_{0} is a
lower cover of γ_{1} and order it as follows:
γ<=δ iff γ_{0} <=
δ_{0}, γ_{1} <=δ_{1}, but
γ_{1} <=δ_{0} does not hold. Let
C(L,γ) denote the connected
component of γ in this poset. Our main result
states that C(L,γ) is a
semidistributive lattice if L is semidistributive,
and that C(L,γ) is a bounded
lattice if L is bounded. Let S_{n} be
the permutohedron on n letters and
T_{n} be the associahedron on n+1
letters. Explicit computations show that
C(S_{n},α) =
S_{n1} and
C(T_{n},α) =
T_{n1}, up to isomorphism, whenever
α is an atom. These results are consequences
of new characterizations of finite join
semidistributive and finite lower bounded lattices:
(i) a finite lattice is join semidistributive if and
only if the projection sending γin
C(L) to γ_{0} inL creates
pullbacks, (ii) a finite join semidistributive
lattice is lower bounded if and only if it has a
strict facet labelling. Strict facet labellings, as
defined here, are generalization of the tools used
by Barbut et al. to prove that lattices of Coxeter
groups are bounded.

[12] 
L. Santocanale, Completions of μalgebras, Annals of Pure and Applied Logic
154 (1) (2008) 2750.
[ EE 
Hal ]
Abstract.
A μalgebra is a model of a first order theory
that is an extension of the theory of bounded
lattices, that comes with pairs of terms
(f,μ_{x}.f) where μ_{x}.f is axiomatized as
the least prefixed point of f, whose axioms are
equations or equational implications. Standard
μalgebras are complete meaning that their
lattice reduct is a complete lattice. We prove that
any non trivial quasivariety of μalgebras
contains a μalgebra that has no embedding into
a complete μalgebra. We focus then on modal
μalgebras, i.e. algebraic models of the
propositional modal μcalculus. We prove that
free modal μalgebras satisfy a condition 
reminiscent of Whitman's condition for free lattices
 which allows us to prove that (i) modal operators
are adjoints on free modal μalgebras, (ii)
least prefixed points of Σ_{1}operations
satisfy the constructive relation μ_{x}.f =
_{n >=0} f^{n}(). These properties
imply the following statement: the
MacNeilleDedekind completion of a free modal
μalgebra is a complete modal μalgebra and
moreover the canonical embedding preserves all the
operations in the class Comp(Σ_{1},Π_{1})
of the fixed point alternation hierarchy.

[13] 
L. Santocanale, On the join depenency relation in multinomial lattices, Order
24 (3) (2007) 155179.
[ EE 
Hal ]
Abstract.
We study the congruence lattices of the multinomial
lattices L(v) introduced by Bennett and
Birkhoff. Our main motivation is to investigate
Parikh equivalence relations that model concurrent
computation. We accomplish this goal by providing an
explicit description of the join dependency relation
between two join irreducible elements and of its
reflexive transitive closure. The explicit
description emphasizes several properties and makes
it possible to separate the equational theories of
multinomial lattices by their dimensions. In their
covering of non modular varieties Jipsen and Rose
define a sequence of equations SD_{n}(/\), for
n >=0. Our main result sounds as follows:
if v = (v_{1},...,v_{n}) belongs to N^{n} and
v_{i} > 0 for i = 1,...,n, then the
multinomial lattice L(v) satisfies
SD_{n1}(/\) and fails SD_{n2}(/\).

[14] 
A. Arnold, L. Santocanale, Ambiguous classes in μcalculi hierarchies,
Theoretical Computer Science 333 (12) (2005) 265296.
[ EE ]
Abstract.
A classical result by Rabin states that if a set of
trees and its complement are both Büchi definable
in the monadic second order logic, then these sets
are weakly definable. In the language of
μcalculi, this theorem asserts the equality
between the complexity classes Σ_{2} /\
Π_{2} and Comp(Σ_{1},Π_{1}) of the
alternationdepth hierarchy of the μcalculus of
tree languages. It becomes natural to ask whether at
higher levels of the hierarchy the ambiguous classes
Σ_{n + 1} /\Π_{n + 1} and the
composition classes Comp(Σ_{n},Π_{n}) are
equal, and for which μcalculi. A first result
of this paper is that the alternationdepth
hierarchy of the games μcalculus  whose
canonical interpretation is the class of all
complete lattices  enjoys this
property. Explicitly, every parity game which is
equivalent both to a game in Σ_{n + 1} and to
a game in Π_{n + 1} is also equivalent to a game
obtained by composing games in Σ_{n} and
Π_{n}. A second result is that the
alternationdepth hierarchy of the μcalculus of
tree languages does not enjoy the property. Taking
into account that any Büchi definable set is
recognized by a nondeterministic Büchi automaton,
we generalize Rabin's result in terms of the
following separation theorem: if two disjoint
languages are recognized by nondeterministic
Π_{n+ 1} automata, then there exists a third
language recognized by an alternating automata in
Comp(Σ_{n},Π_{n}) containing one and
disjoint with the other. Finally, we lift the
results obtained for the μcalculus of tree
languages to the propositional modal μcalculus:
ambiguous classes do not coincide with composition
classes, but a separation theorem is established for
disjunctive formulas.

[15] 
R. Cockett, L. Santocanale, Induction, coinduction, and adjoints, Electronic
Notes in Theoretical Computer Science 69 (2003) 101119, CTCS'02, Category
Theory and Computer Science 2002.
[ EE 
.ps ]
Abstract.
We investigate the reasons for which the existence
of certain right adjoints implies the existence of
some final coalgebras, and viceversa. In particular
we prove and discuss the following theorem which has
been partially available in the literature: let F
G be a pair of adjoint functors, and suppose
that an initial algebra F(X) of the functor H(Y)
= X + F(Y) exists; then a right adjoint G(X) to
F(X) exists if and only if a final coalgebra
HG(X) of the functor K(Y) = X ×G(Y)
exists. Motivated by the problem of understanding
the structures that arise from initial algebras, we
show the following: if F is a left adjoint with a
certain commutativity property, then an initial
algebra of H(Y) = X + F(Y) generates a subcategory
of functors with inductive types where the
functorial composition is constrained to be a
Cartesian product.

[16] 
L. Santocanale, On the equational definition of the least prefixed point,
Theoretical Computer Science 295 (13) (2003) 341370.
[ EE ]
Abstract.
We propose a method to axiomatize by equations the
least prefixed point of an order preserving
function. We discuss its domain of application and
show that the Boolean μcalculus has a complete
equational axiomatization. The method relies on the
existence of a "closed structure" and its
relationship to the equational axiomatization of
Action Logic is made explicit. The implication
operation of a closed structure is not monotonic in
one of its variables; we show that the existence of
such a term that does not preserve the order is an
essential condition for defining by equations the
least prefixed point. We stress the interplay
between closed structures and fixed point operators
by showing that the theory of Boolean modal
μalgebras is not a conservative extension of
the theory of modal μalgebras. The latter is
shown to lack the finite model property.

[17] 
L. Santocanale, μbicomplete categories and parity games, Theoretical
Informatics and Applications 36 (2002) 195227.
[ EE ]
Abstract.
For an arbitrary category, we consider the least
class of functors containing the projections and
closed under finite products, finite coproducts,
parameterized initial algebras and parameterized
final coalgebras, i.e. the class of functors that
are definable by μterms. We call the category
μbicomplete if every μterm defines a
functor. We provide concrete examples of such
categories and explicitly characterize this class of
functors for the category of sets and
functions. This goal is achieved through parity
games: we associate to each game an algebraic
expression and turn the game into a term of a
categorical theory. We show that μterms and
parity games are equivalent, meaning that they
define the same property of being
μbicomplete. Finally, the interpretation of a
parity game in the category of sets is shown to be
the set of deterministic winning strategies for a
chosen player.

[18] 
L. Santocanale, Free μlattices, Journal of Pure and Applied Algebra
168 (23) (2002) 227264.
[ EE ]
Abstract.
A μlattice is a lattice with the property that
every unary polynomial has both a least and a
greatest fixpoint. In this paper we define the
quasivariety of μlattices and, for a given
partially ordered set P, we construct a
μlattice J_{P} whose elements are
equivalence classes of games in a preordered class
J(P). We prove that the μlattice
J_{P} is free over the ordered set P and
that the order relation of J_{P} is
decidable if the order relation of P is
decidable. By means of this characterization of free
μlattices we infer that the class of complete
lattices generates the quasivariety of
μlattices.

[19] 
L. Santocanale, The alternation hierarchy for the theory of μlattices,
Theory and Applications of Categories 9 (2002) 166197.
[ Journal ]
Abstract.
The alternation hierarchy problem asks whether every
μterm φ, that is, a term built up also
using a least fixed point constructor as well as a
greatest fixed point constructor, is equivalent to a
μterm where the number of nested fixed points
of a different type is bounded by a constant
independent of φ. In this paper we give a proof
that the alternation hierarchy for the theory of
μlattices is strict, meaning that such a
constant does not exist if μterms are built up
from the basic lattice operations and are
interpreted as expected. The proof relies on the
explicit characterization of free μlattices by
means of games and strategies.

Articles in conference proceedings
[1] 
L. Santocanale, The equational theory of the natural join and inner union is
decidable, in: C. Baier, U. D. Lago (eds.), Foundations of Software Science
and Computation Structures  21st International Conference, FOSSACS 2018,
Held as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2018, Thessaloniki, Greece, April 1420, 2018, Proceedings,
vol. 10803 of Lecture Notes in Computer Science, Springer, 2018, pp.
494510.
[ EE 
Hal ]
Abstract.
The natural join and the inner union operations
combine relations of a database. Tropashko and
Spight realized that these two operations are
the meet and join operations in a class of lattices,
known by now as the relational lattices. They
proposed then lattice theory as an algebraic
approach to the theory of databases, alternative to
the relational algebra. Previous works
proved that the quasiequational theory of these
lattices—that is, the set of definite Horn sentences
valid in all the relational lattices—is undecidable,
even when the signature is restricted to the pure
lattice signature. We prove here that the equational
theory of relational lattices is decidable. That, is
we provide an algorithm to decide if two lattice
theoretic terms t, s are made equal under all
intepretations in some relational lattice. We
achieve this goal by showing that if an inclusion t
≤ s fails in any of these lattices, then it fails in
a relational lattice whose size is bound by a triple
exponential function of the sizes of t and s.

[2] 
M. J. Gouveia, L. Santocanale, Aleph1 and the Modal muCalculus, in:
V. Goranko, M. Dam (eds.), 26th EACSL Annual Conference on Computer Science
Logic (CSL 2017), vol. 82 of Leibniz International Proceedings in Informatics
(LIPIcs), Schloss DagstuhlLeibnizZentrum fuer Informatik, Dagstuhl,
Germany, 2017, pp. 38:138:16.
[ EE 
Hal ]
Abstract.
For a regular cardinal κ, a formula of the
modal μcalculus is κcontinuous in a
variable x if, on every model, its interpretation
as a unary function of x is monotone and preserves
unions of κdirected sets. We define the
fragment C_{aleph_1}(x) of the modal
μcalculus and prove that all the formulas in
this fragment are aleph_{1}continuous. For each
formula φ(x) of the modal μcalculus, we
construct a formula ψ(x) C_{aleph_1}(x) such
that φ(x) is κcontinuous, for some
κ, if and only if φ(x) is equivalent to
ψ(x). Consequently, we prove that (i) the
problem whether a formula is κcontinuous for
some κ is decidable, (ii) up to equivalence,
there are only two fragments determined by
continuity at some regular cardinal: the fragment
C_{aleph_0}(x) studied by Fontaine and the
fragment C_{aleph_1}(x). We apply our
considerations to the problem of characterizing
closure ordinals of formulas of the modal
μcalculus. An ordinal α is the closure
ordinal of a formula φ(x) if its interpretation
on every model converges to its least fixedpoint in
at most α steps and if there is a model where
the convergence occurs exactly in α steps. We
prove that ω_{1}, the least uncountable
ordinal, is such a closure ordinal. Moreover we
prove that closure ordinals are closed under ordinal
sum. Thus, any formal expression built from 0, 1,
ω, ω_{1} by using the binary operator
symbol + gives rise to a closure ordinal.

[3] 
L. Santocanale, The embeddability for relational lattices is undecidable, in:
Relational and Algebraic Methods in Computer Science  16th International
Conference, RAMiCS 2017, Lyon, France, May 1518, 2017, Proceedings, 2017,
pp. 258273.
[ EE 
Hal ]
Abstract.
The natural join and the inner union operations
combine relations of a database. Tropashko and
Spight realized that these two operations are the
meet and join operations in a class of lattices,
known by now as the relational lattices. They
proposed then lattice theory as an algebraic
approach to the theory of databases alternative to
the relational algebra. Litak et al. proposed an
axiomatization of relational lattices over the
signature that extends the pure lattice signature
with a constant and argued that the quasiequational
theory of relational lattices over this extended
signature is undecidable. We prove in this paper
that embeddability is undecidable for relational
lattices. More precisely, it is undecidable whether
a finite subdirectlyirreducible lattice can be
embedded into a relational lattice. Our proof is a
reduction from the coverability problem of a
multimodal frame by a universal product frame and,
indirectly, from the representability problem for
relation algebras. As corollaries we obtain the
following results: the quasiequational theory of
relational lattices over the pure lattice signature
is undecidable and has no finite base; there is a
quasiequation over the pure lattice signature which
holds in all the finite relational lattices but
fails in an infinite relational lattice.

[4] 
L. Santocanale, Relational lattices via duality, in: I. Hasuo (ed.),
Coalgebraic Methods in Computer Science, CMCS 2016, vol. 9608 of Lecture
Notes in Computer Science, Springer, 2016, pp. 195215.
[ EE 
Hal ]
Abstract.
The natural join and the inner union combine in
different ways tables of a relational
database. Tropashko observed that these two
operations are the meet and join in a class of
latticescalled the relational latticesand
proposed lattice theory as an alternative algebraic
approach to databases. Aiming at query optimization,
Litak et al. initiated the study of the equational
theory of these lattices. We carry on with this
project, making use of the duality theory developed
by us. The contributions of this paper are as
follows. Let A be a set of column's names and D
be a set of cell values; we characterize the dual
space of the relational lattice R(D,A) by means of
a generalized ultrametric space, whose elements are
the functions from A to D, with the
P(A)valued distance being the Hamming one but
lifted to subsets of A. We use the dual space to
present an equational axiomatization of these
lattices that reflects the combinatorial properties
of these generalized ultrametric spaces: symmetry
and pairwise completeness. Finally, we argue that
these equations correspond to combinatorial
properties of the dual spaces of lattices, in a
technical sense analogous of correspondence theory
in modal logic. In particular, this leads an exact
characterization of the finite lattices satisfying
these equations.

[5] 
S. Ghilardi, M. J. Gouveia, L. Santocanale, Fixedpoint elimination in the
intuitionistic propositional calculus, in: B. Jacobs, C. Löding (eds.),
Foundations of Software Science and Computation Structures  19th
International Conference, FOSSACS 2016, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The
Netherlands, April 28, 2016, Proceedings, vol. 9634 of Lecture Notes in
Computer Science, Springer, 2016, pp. 126141.
[ EE 
Hal ]
Abstract.
It is a consequence of existing literature that
least and greatest fixedpoints of monotone
polynomials on Heyting algebrasthat is, the
algebraic models of the Intuitionistic Propositional
Calculusalways exist, even when these algebras are
not complete as lattices. The reason is that these
extremal fixedpoints are definable by formulas of
the IPC. Consequently, the μcalculus based on
intuitionistic logic is trivial, every μformula
being equivalent to a fixedpoint free formula. We
give in this paper an axiomatization of least and
greatest fixedpoints of formulas, and an algorithm
to compute a fixedpoint free formula equivalent to
a given μformula. The axiomatization of the
greatest fixedpoint is simple. The axiomatization
of the least fixedpoint is more complex, in
particular every monotone formula converges to its
least fixedpoint by Kleene's iteration in a finite
number of steps, but there is no uniform upper bound
on the number of iterations. We extract, out of the
algorithm, upper bounds for such n, depending on the
size of the formula. For some formulas, we show that
these upper bounds are polynomial and optimal.

[6] 
S. Frittella, L. Santocanale, Fixedpoint theory in the varieties
D_{n}, in: P. Höfner, P. Jipsen, W. Kahl, M. E. Müller
(eds.), RAMICS, vol. 8428 of Lecture Notes in Computer Science, Springer,
2014, pp. 446462.
[ EE ]
Abstract.
The varieties of lattices D_{n}, n
>=0, were introduced in [Nation90] and studied
later in [Semenova05]. These varieties might be
considered as generalizations of the variety of
distributive lattices which, as a matter of fact,
coincides with D_{0}. It is well known
that least and greatest fixedpoints of terms are
definable on distributive lattices; this is an
immediate consequence of the fact that the equation
φ^{2}() = φ() holds on distributive
lattices, for any lattice term φ(x). In this
paper we propose a generalization of this fact by
showing that the identity φ^{n + 2}(x) = φ^{n
+1}(x) holds in D_{n}, for any lattice
term φ(x) and for x in
,. Moreover, we prove that the
equations φ^{n + 1}(x) = φ^{n}(x), x =
,, might not hold in the variety
D_{n} nor in the variety
D_{n} D_{n}^{op}, where
D_{n}^{op} is the variety containing the
lattices L^{op}, for L inD_{n}.

[7] 
J. Fortier, L. Santocanale, Cuts for circular proofs: semantics and
cutelimination, in: S. R. D. Rocca (ed.), CSL, vol. 23 of LIPIcs, Schloss
Dagstuhl  LeibnizZentrum fuer Informatik, 2013, pp. 248262.
[ EE ]
Abstract.
One of the authors introduced in
[20] a calculus of circular proofs
for studying the computability arising from the
following categorical operations: finite products,
finite coproducts, initial algebras, final
coalgebras. The calculus presented
[20] is cutfree; even if sound and
complete for provability, it lacked an important
property for the semantics of proofs, namely
fullness w.r.t. the class of intended categorical
models (called μbicomplete categories)). In this paper we fix this
problem by adding the cut rule to the calculus and
by modifying accordingly the syntactical constraint
ensuring soundness of proofs. The enhanced proof
system fully represents arrows of the canonical
model (a free μbicomplete category). We also
describe a cutelimination procedure as a a model of
computation arising from the above mentioned
categorical operations. The procedure constructs a
cutfree prooftree with possibly infinite branches
out of a finite circular proof with cuts.

[8] 
Y. Venema, L. Santocanale, Uniform interpolation for monotone modal logic, in:
L. Beklemishev, V. Goranko, V. Shehtman (eds.), Advances in Modal Logic,
Volume 8, College Publications, 2010, pp. 350370.
[ .pdf ]
Abstract.
We reconstruct the syntax and semantics of monotone
modal logic, in the style of Moss' coalgebraic
logic. To that aim, we replace the box and diamond
with a modality nabla which takes a finite
collection of finite sets of formulas as its
argument. The semantics of this modality in monotone
neighborhood models is defined in terms of a version
of relation lifting that is appropriate for this
setting. We prove that the standard modal language
and our r based one are effectively
equiexpressive, meaning that there are effective
translations in both directions. We prove and
discuss some algebraic laws that govern the
interaction of nabla with the Boolean
operations. These laws enable us to rewrite each
formula into a special kind of disjunctive normal
form that we call transparent. For such transparent
formulas it is relatively easy to define the
bisimulation quantifiers that one may associate with
our notion of relation lifting. This allows us to
prove the main result of the paper, viz., that
monotone modal logic enjoys the property of uniform
interpolation.

[9] 
R. Cockett, L. Santocanale, On the word problem for ΣΠcategories,
and the properties of twoway communication, in: E. Grädel, R. Kahle
(eds.), CSL, vol. 5771 of Lecture Notes in Computer Science, Springer, 2009,
pp. 194208.
[ EE 
Hal ]
Abstract.
The word problem for categories with free products
and coproducts (sums), SPcategories, is directly
related to the problem of determining the
equivalence of certain processes. Indeed, the maps
in these categories may be directly interpreted as
processes which communicate by twoway channels. The
maps of an SPcategory may also be viewed as a proof
theory for a simple logic with a game theoretic
intepretation. The cutelimination procedure for
this logic determines equality only up to certain
permuting conversions. As the equality classes under
these permuting conversions are finite, it is easy
to see that equality between cutfree terms (even in
the presence of the additive units) is
decidable. Unfortunately, this does not yield a
tractable decision algorithm as these equivalence
classes can contain exponentially many
terms. However, the rather special properties of
these free categories  and, thus, of twoway
communication  allow one to devise a tractable
algorithm for equality. We show that, restricted to
cutfree terms s,t : X > A, the decision procedure
runs in time polynomial on XA, the product of
the sizes of the domain and codomain type.

[10] 
W. Belkhir, L. Santocanale, The variable hierarchy for the lattice
μcalculus, in: I. Cervesato, H. Veith, A. Voronkov (eds.), LPAR 2008,
vol. 5330 of Lecture Notes in Computer Science, Springer, 2008, pp. 605620,
proceedings of the 15th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning, Doha, Qatar, November 2227, 2008.
[ EE 
Hal ]
Abstract.
Parity games are combinatorial representations of
closed Boolean μterms. By adding to them draw
positions, they have been organized by Arnold and
one of the authors into a μcalculus. As done by
Berwanger et al. for the propositional modal
μcalculus, it is possible to classify parity
games into levels of hierarchy according to the
number of fixedpoint variables. We ask whether this
hierarchy collapses w.r.t. the standard
interpretation of the games μcalculus into the
class of all complete lattices. We answer this
question negatively by providing, for each n >=
1, a parity game G_{n} with these properties: it
unravels to a μterm built up with n
fixedpoint variables, it is semantically equivalent
to no game with strictly less than n2 fixedpoint
variables.

[11] 
L. Santocanale, Combinatorics from concurrency: the nice labelling problem for
event structures, in: Y. Boudabbous, N. Zaguia (eds.), ROGICS'08, 2008, pp.
411419, proceedings of the International Conference on Relations, Orders
and Graphs : Interaction with Computer Science. 1217 May, 2008, Mahdia,
Tunisia.
[ .pdf ]
Abstract.
An event structures is a mathematical model of a
concurrent process. It consists of a set of local
events ordered by a causality relation and separated
by a conflict relation. A global state, or
configuration, is an order ideal whose elements are
pairwise not in conflict. Configurations, ordered by
subset inclusion, form a poset whose Hasse diagram
codes the statetransition graph of the process. By
labelling edges, the statetransition graph can be
enriched with the structure of a deterministic
concurrent automaton on some alphabet. The
nice labelling problem asks to minimize the
cardinality of the alphabet. In this talk we shall
first introduce the nice labelling problem and show
how it translates to a graph coloring problem. We
shall then survey on the problem and present the
results that are available to us nowadays. Thus we
shall The survey will also be the occasion to point
out new perspectives, open problems, and research
paths.

[12] 
W. Belkhir, L. Santocanale, Undirected graphs of entanglement 2, in: V. Arvind,
S. Prasad (eds.), FSTTCS 2007, vol. 4855 of Lecture Notes in Computer
Science, Springer, 2007, pp. 508519, proceedings of the 27th International
Conference on Foundations of Software Technology and Theoretical Computer
Science, New Delhi, India, December 1214, 2007.
[ EE 
Hal ]
Abstract.
Entanglement is a complexity measure of directed
graphs that origins in fixed point theory. This
measure has shown its use in designing efficient
algorithms to verify logical properties of
transition systems. We are interested in the problem
of deciding whether a graph has entanglement at most
k. As this measure is defined by means of games,
game theoretic ideas naturally lead to design
polynomial algorithms that, for fixed k, decide
the problem. Known characterizations of directed
graphs of entanglement at most 1 lead, for k =
1, to design even faster algorithms. In this paper
we present an explicit characterization of
undirected graphs of entanglement at most
2. With such a characterization at hand, we devise
a linear time algorithm to decide whether an
undirected graph has this property.

[13] 
Y. Venema, L. Santocanale, Completeness for flat modal fixpoint logics, in:
N. Dershowitz, A. Voronkov (eds.), LPAR 2007, vol. 4790 of Lecture Notes in
Artificial Intelligence, Springer, 2007, pp. 499513, proceedings of the
14th International Conference on Logic for Programming, Artificial
Intelligence, and Reasoning, Yerevan, Armenia, October 1519, 2007.
[ EE 
.pdf ]
Abstract.
Given a set Γ of modal formulas of the form
γ(x,p), where x occurs positively in
γ, the language L_{#}(Γ) is
obtained by adding to the language of polymodal
logic connectives #_{γ}, γin
Γ. Each term #_{γ} is meant to be
interpreted as the least fixed point of the
functional interpretation of the term
γ(x). Given such a Γ, we construct an
axiom system K_{#}(Γ) which is
sound and complete w.r.t. the concrete
interpretation of the language
L_{#}(Γ) on Kripke frames. If
Γ is finite, then K_{#}(Γ)
is a finite set of axioms and inference rules.

[14] 
L. Santocanale, A nice labelling for treelike event structures of degree 3,
in: L. Caires, V. T. Vasconcelos (eds.), CONCUR 2007, vol. 4703 of Lecture
Notes in Computer Science, Springer, 2007, pp. 151165, proceedings of the
18th International Conference on Concurrency Theory, Lisbon, Portugal,
September 38, 2007.
[ EE 
Hal ]
Abstract.
We address the problem of finding nice labellings
for event structures of degree 3. We develop a
minimum theory by which we prove that the labelling
number of an event structure of degree 3 is
bounded by a linear function of the height. The main
theorem we present in this paper states that event
structures of degree 3 whose causality order is a
tree have a nice labelling with 3 colors. Finally,
we exemplify how to use this theorem to construct
upper bounds for the labelling number of other event
structures of degree 3.

[15] 
L. Santocanale, Completions of μalgebras, in: LICS 2005, IEEE Computer
Society, 2005, pp. 219228, proceedings of the 20th IEEE Symposium on Logic
in Computer Science, 2629 June 2005, Chicago, IL, USA.
[ EE 
.pdf ]
Abstract.
We define the class of algebraic models of
μcalculi and study whether every such model can
be embedded into a model which is a complete
lattice. We show that this is false in the general
case and focus then on free modal μalgebras,
i.e. Lindenbaum algebras of the propositional modal
μcalculus. We prove the following fact: the
MacNeilleDedekind completion of a free modal
μalgebra is a complete modal algebra, hence a
modal μalgebra (i.e. an algebraic model of the
propositional modal μcalculus). The canonical
embedding of the free modal μalgebra into its
DedekindMacNeille completion preserves the
interpretation of all the terms in the class
Comp(Σ_{1},Π_{1}) of the alternationdepth
hierarchy. The proof uses algebraic techniques only
and does not directly rely on previous work on the
completeness of the modal μcalculus.

[16] 
S. Ghilardi, L. Santocanale, Algebraic and model theoretic techniques for
fusion decidability in modal logics, in: M. Y. Vardi, A. Voronkov (eds.),
LPAR 2003, No. 2850 in Lecture Notes in Artificial Intelligence, Springer,
2003, pp. 152166, proceedings of the 10th International Conference Logic
for Programming, Artificial Intelligence, and Reasoning, Almaty, Kazakhstan,
September 2226, 2003.
[ EE 
.pdf ]
Abstract.
We introduce a new method (derived from model
theoretic general combination procedures in
automated deduction) for proving fusion decidability
in modal systems. We apply it to show fusion
decidability in case not only the boolean
connectives, but also a universal modality and
nominals are shared symbols.

[17] 
L. Santocanale, Logical construction of final coalgebras, in: H. P. Gumm (ed.),
Electronic Notes in Theoretical Computer Science, vol. 82, Elsevier, 2003,
pp. 120, proceedings of the workshop Coalgebraic Methods in Computer
Science 2003, Warsaw, Poland, April 2003.
[ EE 
.ps ]
Abstract.
We prove that every finitary polynomial endofunctor
of a category C has a final coalgebra, provided
that C is locally Cartesian closed, it has finite
coproducts and is an extensive category, it has a
natural number object.

[18] 
A. Arnold, L. Santocanale, Ambiguous classes in the games μcalculus
hierarchy, in: A. D. Gordon (ed.), FOSSACS 2003, No. 2620 in Lecture Notes in
Computer Science, Springer, 2003, pp. 7086, proceedings of the 6th
International Conference on Foundations of Software Science and Computation
Structures. Held as Part of the Joint European Conferences on Theory and
Practice of Software, ETAPS 2003. Warsaw, Poland, April 2003.
[ EE 
.ps ]
Abstract.
Every parity game is a combinatorial representation
of a closed Boolean μterm. When interpreted in
a distributive lattice every Boolean μterm is
equivalent to a fixedpoint free term. The
alternationdepth hierarchy is therefore trivial in
this case. This is not the case for non distributive
lattices, as the second author has shown that the
alternationdepth hierarchy is infinite. In this
paper we show that the alternationdepth hierarchy
of the games μcalculus, with its interpretation
in the class of all complete lattices, has a nice
characterization of ambiguous classes: every parity
game which is equivalent both to a game in
Σ_{n + 1} and to a game in Π_{n + 1} is
also equivalent to a game obtained by composing
games in Σ_{n} and Π_{n}.

[19] 
L. Santocanale, From parity games to circular proofs, in: L. S. Moss (ed.),
Electronic Notes in Theoretical Computer Science, vol. 65, Elsevier Science
Publishers, 2002, pp. 112, extended abstract of an invited talk at the
workshop CMCS'2002, Coalgebraic Methods in Computer Science.
[ EE 
.ps ]
Abstract.
We survey on the ongoing research that relates the
combinatorics of parity games to the algebra of
categories with finite products, finite coproducts,
initial algebras and final coalgebras of definable
functors, i.e. μbicomplete categories. We argue
that parity games with a given starting position
play the role of terms for the theory of
μbicomplete categories. We show that the
interpretation of a parity game in the category of
sets and functions is the set of deterministic
winning strategies for one player in the game. We
discuss bounded memory communication strategies
between two parity games and their computational
significance. We describe how an attempt to
formalize them within the algebra of
μbicomplete categories leads to develop a
calculus of proofs that are allowed to contain
cycles.

[20] 
L. Santocanale, A calculus of circular proofs and its categorical semantics,
in: M. Nielsen, U. Engberg (eds.), FOSSACS 2002, No. 2303 in Lecture Notes in
Computer Science, Springer, 2002, pp. 357371, proceedings of the 5th
International Conference on Foundations of Software Science and Computation
Structures. Held as Part of the Joint European Conferences on Theory and
Practice of Software, ETAPS 2002 Grenoble, France, April 812, 2002.
[ EE 
.ps ]
Abstract.
We present a calculus of “circular proofs”: the
graph underlying a proof is not a finite tree but
instead it is allowed to contain a certain amount of
cycles. The main challenge in developing a theory
for the calculus is to define the semantics of
proofs, since the usual method by induction on the
structure is not available. We solve this problem by
associating to each proof a system of equations 
defining relations among undetermined arrows of an
arbitrary category with finite products and
coproducts as well as constructible initial algebras
and final coalgebras  and by proving that this
system admits always a unique solution.

[21] 
L. Santocanale, On the equational definition of the least prefixed point, in:
J. Sgall, A. Pultr, P. Kolman (eds.), MFCS 2001, No. 2136 in Lecture Notes in
Computer Science, Springer, 2001, pp. 645656, procedings of the 26th
International Symposium on Mathematical Foundations of Computer Science 2001,
Marianske Lazne, Czech Republic, August 2731, 2001.
[ EE 
.ps ]
Abstract.
We show how to axiomatize by equations the least
prefixed point of an order preserving function and
discuss the domain of application of the proposed
method. Thus, we generalize the well known
equational axiomatization of Propositional Dynamic
Logic to a complete equational axiomatization of the
Boolean Modal μCalculus. We show on the other
hand that the existence of a term which does not
preserve the order is an essential condition for the
least prefixed point to be definable by equations.

Chapters in books
[1]  N. Caspard, L. Santocanale, F. Wehrung, Algebraic and combinatorial aspects of permutohedra, in: G. Gratzer, F. Wehrung (eds.), Lattice Theory: Special Topics and Applications, Birkhäuser Basel, 2016, pp. 215286. [ EE ] 
[2]  L. Santocanale, F. Wehrung, Generalizations of the permutohedron: Closedopen constructions, in: G. Gratzer, F. Wehrung (eds.), Lattice Theory: Special Topics and Applications, Birkhäuser Basel, 2016, pp. 287397. [ EE ] 
Preprints
[1] 
L. Santocanale, A duality for finite lattices, unpublished (Nov. 2009).
[ Hal ]
Abstract.
A presentation is a triple
X,<=,M with X,<= a
finite poset and M : X ((X))  these
data being subject to additional constraints. Given
a presentation we can define closed subsets of X,
whence a finite lattice. Given a finite lattice L,
we can define its presentation: X is the set of
joinirreducible elements of L, <= is the
restriction of the order to joinirreducible
elements, and M(x) is the set of minimal
joincovers of x. Morphisms of presentations can
be defined as some zigzag relations. Our main
result is: the category of presentations is
dually equivalent to the category of finite
lattice. The two constructions described above are
the object part of contravariant functors giving
rise to the duality. We think of presentations as
semantic domains for lattice terms and formulas of
substructural logics. Relying on previous work by
Nation and Semenova, we show that some equational
properties of finite lattices correspond to first
order properties of presentations. Namely, for each
finite tree T, we construct an equation e_T
that holds in a finite lattice if and only its
presentation does not have some a shape from T. We
illustrate further use of these semantics within the
theory of fixed points over finite lattices: we
generalize, in a nontrivial way, the well known
fact that least fixed points on distributive lattice
terms can be eliminated.

[2] 
L. Santocanale, Logical construction of final coalgebras (Feb. 2004).
[ Hal 
.ps ]
Abstract.
We prove that every finitary polynomial endofunctor
of a category C has a final coalgebra if
C is locally Cartesian closed, has
finite disjoint coproducts and a natural number
object. More generally, we prove that the category
of coalgebras for such an endofunctor has all finite
limits.

[3] 
G. Meloni, L. Santocanale, Relational semantics for distributive linear logic
(Aug. 1995).
[ .ps 
.ps ]
Abstract.
We have investigated axioms related to linear
negation in the context of intuitionistic
generalization of complete semantics for
Distributive Linear Logic presented in [GM]. We show
that internal monoids in the monoidal category of
bimodules between partially ordered sets provide a
complete semantics for Linear Logic based on
intuitionism. The basic framework is a set with a
partial order and a ternary relation which satisfies
compatibility conditions with the order, as also
shown in [AD]. We give concrete examples of such
structures: one of them is suggested by an immediate
generalization to intuitionism of the quantale of
all relations over a set; another universe can be
obtained by putting together all the individuals of
a monoid in presheaves. The analysis in this context
of axioms ruling linear negation has followed the
suggestion in [Yet]: condition of being a dualizing
element and condition of being a cyclic element have
been analyzed separately. Since the starting point
of our work has been the observation that groupoids
are models not only for linear logic, but also for
classical linear logic when a proper choice of
linear false is done, we have investigated also
syntactic conditions which are always valid in these
particular universes. These are a noncontradiction
principle which merges cartesian conjunction with
linear negation and true, and De Morgan laws of
complement with respect to linear conjunction and
disjunction. In the classical case the non
contradiction principle is equivalent to take as
linear false the complement of unity. This choice
leads in groupoids to satisfy De Morgan laws which
are however not derivable; which is proved by
construction of counterexamples. Quantifiers
elimination by means of properties of the free
algebra of lower sets has been the general method
followed in the analysis from syntax to semantics. A
second part of the work has confronted the opposite
problem: given semantic conditions we show that,
from their truth in the canonical model of prime
filters, equivalent syntactic conditions are
found. In this case an analogous way of eliminating
quantifiers over prime filters needs the extensive
use of Extension/Exclusion Lemma which requires the
axiom of choice. Beside the problem of extending a
theory in which a syntactic condition holds to a
complete one, there is the research of syntactic
equivalents to interesting semantic conditions. [AD]
G. Allwein  J.M. Dunn, Kripke Models for Linear
Logic, The Journal of Symbolic Logic, Volume 58,
Number 2, (1993), pp. 514545; [GM] S. Ghilardi 
G. Meloni, Modal logics with nary connectives,
Zeitschr.f.math.Logik und Grundlagen d.Math.,
Bd. 36, S.193215 (1990); [Yet] D.N. Yetter,
Quantales and (noncommutative) linear logic, The
Journal of Symbolic Logic, Volume 55, Number 1,
(1990), pp. 4164;

Abstracts
[1]  L. Santocanale, Derived semidistributive lattices, presented at the conference OAL 2007, Nashville, USA, june 12 2007 (Jan. 2007). [ .pdf ] 
[2]  R. Cockett, L. Santocanale, Properties of free σπcategories (short abstract), in: D. Pronk, M. Dawson (eds.), Category Theory 2006, University of Dalhausie, 2006, book of abstracts. 
[3]  A. Arnold, L. Santocanale, On ambiguous classes in the μcalculus hierarchy of tree languages, in: Z. Ésik, I. Walukiewicz (eds.), FICS'03, 2003, pp. 413, proceedings of the workshop Fixed Points in Computer Science 2003. 
[4] 
L. Santocanale, Congruences of modal μalgebras, in: Z. Ésik,
A. Ingólfsdóttir (eds.), FICS02, vol. NS0202 of BRICS Notes Series,
2002, pp. 8387, a refereed extended abstract.
Abstract.
If f(y) is an order preserving endofunction of a
closed ordered monoid, then the two inequations
align* f(g(x))x & <=g(x) & g(f(x)
x) & <=x align* determine an
order preserving endofunction g(x) as
μ_{y}.(f(y) x), the parameterized least
prefixed point of f(y) x. This observation
is the core of a method to axiomatize by equations
the least prefixed point. When this method is
applied to the propositional Boolean modal
μcalculus, it shows that Kozen's axiomatization
can be turned into an equivalent equational
axiomatization that is complete with respect to
Kripke frames by Walukiewicz's theorem. Being able
to equationally axiomatize the propositional Boolean
modal μcalculus implies that its algebraic
models form a variety of algebras, in the usual
sense. We call these models modal
μalgebras. The main characteristic that
distinguishes a variety from a quasivariety 
i.e. a class of models that can be axiomatized by
equational implications  is that such a class is
closed under homomorphic images defined from
congruences. Thus, in a variety of algebras, there
is always a bijection between quotients of an
algebra (categorically, strong epimorphisms) and
congruences on the algebra. Modal μalgebras are
therefore closed under homomorphic images; we have
investigated congruences of modal μalgebras and
found a characterization suitable for algebraic
computations. In this talk we will present this
characterization and illustrate its use by lifting
some classical results from modal logic and modal
algebras to the setting of modal μalgebras. The
characterization of congruences can also be
exploited in the context of verification of systems,
as these results can be reformulated in a logical
framework. For example, it could be useful to
analyze a restricted class of transition systems
where given subsets of states are known to satisfy a
finite number of algebraic relations. Some
propositions of the modal μcalculus could hold
true in these models, and it would be desirable to
know whether their truth is a consequence of Kozen's
axiomatization and of those algebraic
relations. This is a particular instance of a common
problem in logic: is a proposition derivable from a
finite set of propositions that are assumed as
axioms? Among the results that we present is a
deduction theorem for the propositional Boolean
modal μcalculus; this theorem allows to reduce
derivability from a finite set of axioms to
derivability from no axioms. As the latter problem
is well known to be decidable for the modal
μcalculus, then derivability from a finite set
of propositions becomes decidable as well.

[5]  L. Santocanale, μbicomplete categories and parity functors, in: A. Labella (ed.), Abstracts of the Talks of the Workshop on Fixed Point in Computer Science, FICS '01, (Florence, Italy, September 7 and 8, 2001), 2001, a refereed extended abstract, 8pp. [ .ps ] 
[6]  L. Santocanale, The theory of mulattices, in: I. Guessarian (ed.), Abstracts of the Talks of the Workshop on Fixed Points in Computer Science, FICS'00, (Paris, France, July 22 and 23, 2000), 2000, a refereed short abstract. [ .ps ] 
[7]  L. Santocanale, The alternation hierarchy for the theory of μlattices (extended abstract), in: Abstracts from the International Summer Conference in Category Theory, CT2000 (Como, Italy, July 1622, 2000), 2000, a refereed extended abstract. [ .ps ] 
[8]  L. Santocanale, Free μlattices (short abstract), in: J. Adamék (ed.), Abstracts from the Conference on Category Theory 99 (Coimbra, Portugal, July 1924, 1999), Universade de Coimbra, Portugal, 1999, short abstract. 
[9]  L. Santocanale, Distributive non commutative linear logic (short abstract), in: I. U. o. History, P. o. Science (eds.), Volume of abstracts of the 10th International Congress of Logic, Methodology and Philosophy of Science, August 1925, 1995  Florence, Italy, 1995, pp. 6161, a refereed short abstract. 
Technical reports
[1]  L. Santocanale, μbicomplete categories and parity games, Tech. Rep. RR128102, LaBRI, Université Bordeaux 1 (Sep. 2002). [ Hal  http  .ps.gz ] 
[2]  L. Santocanale, On the equational definition of the least prefixed point, Tech. Rep. PIMS021, Pacif Institute for Mathematical Sciences (May 2002). [ http ] 
[3] 
L. Santocanale, A calculus of circular proofs and its categorical semantics,
Tech. Rep. RS0115, BRICS, Department of Computer Science, University of
Aarhus, 30 pp. (May 2001).
[ http ]
Abstract.
We present a calculus of proofs, the intended models
of which are categories with finite products and
coproducts, initial algebras and final coalgebras of
functors that are recursively constructible out of
these operations, that is, μbicomplete
categories. The calculus satisfies the cut
elimination and its main characteristic is that the
underlying graph of a proof is allowed to contain a
certain amount of cycles. To each proof of the
calculus we associate a system of equations which
has a meaning in every μbicomplete
category. We prove that this system admits always a
unique solution, and by means of this theorem we
define the semantics of the calculus

[4] 
L. Santocanale, The alternation hierarchy for the theory of μlattices,
Tech. Rep. RS0029, BRICS, Department of Computer Science, University of
Aarhus, 44 pp. Extended abstract appears in Abstracts from the
International Summer Conference in Category Theory, CT2000, Como, Italy,
July 1622, 2000. Appears in Theory and Applications of Categories, Volume
9, CT2000, pp. 166197 (Nov. 2000).
[ http ]
Abstract.
The alternation hierarchy problem asks whether every
μterm, that is a term built up using also a
least fixed point constructor as well as a greatest
fixed point constructor, is equivalent to a
μterm where the number of nested fixed point of
a different type is bounded by a fixed
number.In this paper we give a proof that
the alternation hierarchy for the theory of μ
lattices is strict, meaning that such number does
not exist if μterms are built up from the basic
lattice operations and are interpreted as
expected. The proof relies on the explicit
characterization of free μlattices by means of
games and strategies

[5] 
L. Santocanale, Free μlattices, Research Series RS0028, BRICS,
Department of Computer Science, University of Aarhus, 51 pp. Short abstract
appeared in Proceedings of Category Theory 99, Coimbra, Portugal, July
1924, 1999. Full version appears in the Journal of Pure and Applied
Algebra, 168/23, pp. 227264 (Nov. 2000).
[ http ]
Abstract.
A μlattice is a lattice with the property that
every unary polynomial has both a least and a
greatest fixpoint. In this paper we define the
quasivariety of μlattices and, for a given
partially ordered set P, we construct a
μlattice J_{P} whose elements are
equivalence classes of games in a preordered class
J(P). We prove that the μlattice
J_{P} is free over the ordered set P and
that the order relation of J_{P} is
decidable if the order relation of P is
decidable. By means of this characterization of free
μlattices we infer that the class of complete
lattices generates the quasivariety of
μlattices

Miscellanea
[1] 
L. Santocanale, On finite circular codes, research notes (feb 1998).
[ .ps ]
Abstract.
Un code est essentiellement la base d'un
sousmonoïde libre d'un monoïde libre (l'ensemble de
tous les mots sur un alphabet). Un code est
circulaire si l'image (par l'inclusion) d'un mot
primitif est primitif et si les images inverses de
deux mots conjugues sont conjugues. Il existe une
sousclasse de codes circulaires, celle des codes
uniformément synchrones. Un résultat bien connu nous
dit qu'un code circulaire fini est toujours
uniformément synchrone. Cependant la preuve contenue
dans l'ouvrage classique sur la théorie des codes
utilise des outils raffines de la théorie de la
reconnaissance des codes par des représentations non
ambiguës sur de monoïdes de relations. Cet expose
donnera une petite introduction à la théorie et
procédera à la preuve de ce résultat de façon
"simple", à l'aide de calculs sur les mots
seulement.

[2]  L. Santocanale, Algebraic topology and distributed computing, work for PhD course at UQÀM. [ .ps ] 
[3]  L. Santocanale, Characterization of analytic functors, work for PhD course at UQÀM. [ .ps ] 
[4]  L. Santocanale, Completeness of algebraic varieties, work for PhD course at UQÀM. [ .ps ] 
[5]  L. Santocanale, Completeness of exponential families, work for PhD course at UQÀM. [ .ps ] 
Tesi di laurea
[1]  L. Santocanale, Semantica relazionale per la logica lineare distributiva, Master's thesis, Università degli Studi di Milano, tesi di laurea (Dec. 1994). [ .pdf ] 
PhD Thesis
[1] 
L. Santocanale, Sur les μtreillis libres, Ph.D. thesis, Université du
Québec à Montréal (Apr. 2000).
[ .ps 
.pdf ]
Abstract.
Un μtreillis est un treillis L avec la
propriété que tout polynôme avec
coefficients dans L possède à la fois un
plus petit point préfixe et un plus grand point
postfixe. Dans ce travail nous définissons la
quasivariété des μtreillis et, pour un
ensemble partiellement ordonné P, nous
construisons un μtreillis J_{P} dont
les éléments sont des classes
d'équivalence de jeux appartenants à une
classe préordonnée J(P). Nous
montrons que le μtreillis J_{P} est
libre sur l'ensemble ordonné P et que la
relation d'ordre de J_{P} est
décidable si la relation d'ordre de P est
décidable. À l'aide de cette
caractérisation nous montrons que la
variété équationelle des μtreillis
est engendrée par la classe des treillis
complets.

Habilitation à diriger les recherches
[1] 
L. Santocanale, Structures algébriques et d'ordre en logique et concurrence,
Habiltation à Diriger les Recherches, Université de Provence (Dec.
2008).
[ Tel ]
Abstract.
Nous souhaitons illustrer comment la notion de
structure, algébrique et d'ordre, peut être un
guide fructuex dans l'étude de sujets importants
de l'informatique tels que les processus concurrents
et les logiques modales et temporales pour la
vérification des systèmes informatiques.
