Daniela Petrisan
Assistant Professor, IRIF, Paris 7
I am an
Assistant Professor at the University Paris Diderot
(Paris 7) and member of
the IRIF
research laboratory. Before that, I was a
postdoctoral researcher working on the ERC
project DuaLL
in the same laboratory. Before joining IRIF I worked
in the Intelligent Systems group at Radboud
University Nijmegen and I was a researcher on the ANR
project PiCoq in
the Plume
team of École
Normale Supérieure Lyon. Previously I had various
positions including a fixedterm lectureship and a
research associate position at
the University of
Leicester.
Contact: petrisanirif.fr
News
Publications
dblp
Teaching
Activities
CV
Contact
Most recent (full list here)
 UpTo Techniques for Behavioural Metrics via Fibrations.
Filippo Bonchi, Barbara König and Daniela Petrisan, CONCUR 2018
[pdf]
[abstract]
Upto
techniques are a wellknown method for enhancing
coinductive proofs of behavioural equi valences. We
introduce upto techniques for behavioural metrics
between systems modelled as coalgebras and we provide
abstract results to prove their soundness in a
compositional way. In order to obtain a general
framework, we need a systematic way to lift functors: we
show that the Wasserstein lifting of a functor,
introduced in a previous work, corresponds to a change
of base in a fibrational sense. This observation enables
us to reuse existing results about soundness of upto
techniques in a fibrational setting. We focus on the
fibrations of predicates and relations valued in a
quantale, for which pseudometric spaces are an
example. To illustrate our approach we provide an
example on distances between regular languages.
 Automata and minimization.
Thomas Colcombet, Daniela Petrisan, SIGLOG News 4(2): 427 (2017)
[link]
[abstract]
Already in
the seventies, strong results illustrating the intimate
relationship between category theory and automata theory
have been described and are still investigated. In this
column, we provide a uniform presentation of the basic
concepts that underlie minimization results in automata
theory. We then use this knowledge for introducing a new
model of automata that is an hybrid of deterministic
finite automata and automata weighted over a
field. These automata are very natural, and enjoy
minimization result by design.
The presentation of this paper is indeed categorical in
essence, but it assumes no prior knowledge from the
reader. It is also nonconventional in that it is
neither algebraic, nor coalgebraic oriented.
 A general account of coinduction upto,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, Acta Informatica, (2016)
[link]
[abstract]
[bibtex]
@Article{BPPR2016,
author={Bonchi, Filippo
and Petri{\c{s}}an, Daniela
and Pous, Damien
and Rot, Jurriaan},
title={A general account of coinduction upto},
journal=[Acta Informatica},
year={2016},
pages={164},
issn={14320525},
doi={10.1007/s0023601602714},
url={http://dx.doi.org/10.1007/s0023601602714},
}
Bisimulation upto enhances the coinductive proof
method for bisimilarity, providing efficient proof techniques
for checking properties of different kinds of systems. We
prove the soundness of such techniques in a fibrational
setting, building on the seminal work of Hermida and
Jacobs. This allows us to systematically obtain upto
techniques not only for bisimilarity but for a large class of
coinductive predicates modeled as coalgebras. The fact that
bisimulations up to context can be safely used in any language
specified by GSOS rules can also be seen as an instance of our
framework, using the wellknown observation by Turi and
Plotkin that such languages form bialgebras. In the second
part of the paper, we provide a new categorical treatment of
weak bisimilarity on labeled transition systems and we prove
the soundness of upto context for weak bisimulations of
systems specified by cool rule formats, as defined by Bloom to
ensure congruence of weak bisimilarity. The weak transition
systems obtained from such cool rules give rise to lax
bialgebras, rather than to bialgebras. Hence, to reach our
goal, we extend the categorical framework developed in the
first part to an ordered setting.
 Automata in the Category of Glued Vector Spaces
Thomas Colcombet, Daniela Petrisan, MFCS 2017
[link]
[abstract]
In this
paper we adopt a categorytheoretic approach to the
conception of automata classes enjoying minimization by
design. The main instantiation of our construction is a
new class of automata that are hybrid between
deterministic automata and automata weighted over a
field.
 Automata minimization: a functorial approach
Thomas Colcombet, Daniela Petrisan, CALCO 2017
[link]
[abstract]
In this
paper we regard languages and their acceptors  such as
deterministic or weighted automata, transducers, or
monoids  as functors from input categories that
specify the type of the languages and of the machines
to categories that specify the type of outputs. Our
results are as follows: a) We provide sufficient
conditions on the output category so that minimization
of the corresponding automata is guaranteed. b) We show
how to lift adjunctions between the categories for
output values to adjunctions between categories of
automata. c) We show how this framework can be applied
to several phenomena in automata theory, starting with
determinization and minimization (previously studied
from a coalgebraic and duality theoretic
perspective). We apply in particular these techniques
to Choffrut’s minimization algorithm for subsequential
transducers and revisit Brzozowski’s minimization
algorithm.
 Quantifiers on languages and codensity monads,
Mai Gehrke, Daniela Petrisan, Luca Reggio, LICS 2017
[link]
[abstract]
[arxiv long version]
[conference version]
This
paper contributes to the techniques of topoalgebraic
recognition for languages beyond the regular setting as
they relate to logic on words. In particular, we
provide a general construction on recognisers
corresponding to adding one layer of various kinds of
quantifiers and prove a related Reutenauertype
theorem. Our main tools are codensity monads and
duality theory. Our construction yields, in particular,
a new characterisation of the profinite monad of the
free Ssemimodule monad for finite and commutative
semirings S, which generalises our earlier insight that
the Vietoris monad on Boolean spaces is the codensity
monad of the finite powerset functor.
 The Schutzenberger Product for Syntactic Spaces. ,
M. Gehrke, D. Petrisan, L. Reggio, ICALP 2016
[link]
[abstract]
Starting from Boolean algebras of languages closed under
quotients and using duality theoretic insights, we derive the
notion of Boolean spaces with internal monoids as recognisers
for arbitrary formal languages of finite words over finite
alphabets. This leads to recognisers and syntactic spaces in a
setting that is wellsuited for applying tools from Stone
duality as applied in semantics. The main focus of the paper
is the development of topoalgebraic constructions pertinent
to the treatment of languages given by logic formulas. In
particular, using the standard semantic view of quantification
as projection, we derive a notion of Schützenberger product
for Boolean spaces with internal monoids. This makes heavy use
of the Vietoris construction  and its dual functor  which is
central to the coalgebraic treatment of classical modal
logic. We show that the unary Schützenberger product for
spaces yields a recogniser for the language of all models of
the formula EXISTS x.phi(x), when applied to a recogniser for
the language of all models of phi(x). Further, we generalise
global and local versions of the theorems of Schützenberger
and Reutenauer characterising the languages recognised by the
binary Schützenberger product. Finally, we provide an
equational characterisation of Boolean algebras obtained by
local Schützenberger product with the one element space based
on an EgliMilner type condition on generalised factorisations
of ultrafilters on words.
 Lax Bialgebras and UpTo Techniques
for Weak Bisimulations,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CONCUR 2015
[abstract]
Upto techniques are useful tools for optimising proofs of
behavioural equivalence of processes. Bisimulations upto
context can be safely used in any language specified by GSOS
rules. We showed this result in a previous paper by exploiting
the wellknown observation by Turi and Plotkin that such
languages form bialgebras. In this paper, we prove the
soundness of upto contextual closure for weak bisimilations
of systems specified by cool rule formats, as defined by Bloom
to ensure congruence of weak bisimilarity. However, the weak
transition systems obtained from such cool rules give rise to
lax bialgebras, rather than to bialgebras. Hence, to reach
our goal, we extend our previously developed categorical
framework to an ordered enriched setting.
 Nominal techniques for variables with interleaving scopes,
D. Ghica, M.J. Gabbay, D. Petrisan. CSL 2015

Nominal Kleene Coalgebra,
D. Kozen, K. Mamouras, D. Petrisan, A. Silva, ICALP 2015
[abstract]
[long version]
We develop the coalgebraic theory of nominal Kleene algebra,
including an alternative languagetheoretic semantics, a
nominal extension of the Brzozowski derivative, and a
bisimulationbased decision procedure for the equational
theory.

Approximation of Nested Fixpoints  A Coalgebraic View of Parametric Dataypes,
A. Kurz, A. Pardo, D. Petrisan, P. Severi and FJ. de Vries, CALCO 2015
[abstract]
The question addressed in this paper is how to correctly
approximate infinite data given by systems of simultaneous
corecursive definitions. We devise a categorical framework
for reasoning about regular datatypes, that is, datatypes
closed under products, coproducts and fixpoints. We argue that
the right methodology is on one hand coalgebraic (to deal with
possible nontermination and infinite data) and on the other
hand 2categorical (to deal with parameters in a disciplined
manner). We prove a coalgebraic version of Beki{\v c} lemma
that allows us to reduce simultaneous fixpoints to a single
fix point. Thus a possibly infinite object of interest is
regarded as a final coalgebra of a manysorted polynomial
functor and can be seen as a limit of finite approximants. As
an application, we prove correctness of a generic function
that calculates the approximants on a large class of data
types.

Coinduction upto in a fibrational setting,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CSLLICS 2014
[link]
[arxiv link]
[conference version]
[abstract]
[bibtex]
@inproceedings{DBLP:conf/csl/BonchiPPR14,,
author = {Filippo Bonchi and
Daniela Petrisan and
Damien Pous and
Jurriaan Rot},
title = {Coinduction upto in a fibrational setting},
booktitle = {Joint Meeting of the TwentyThird {EACSL} Annual Conference on Computer
Science Logic {(CSL)} and the TwentyNinth Annual {ACM/IEEE} Symposium
on Logic in Computer Science (LICS), {CSLLICS} '14, Vienna, Austria,
July 14  18, 2014},
pages = {20},
year = {2014},
url = {http://doi.acm.org/10.1145/2603088.2603149},
doi = {10.1145/2603088.2603149},
}
Bisimulation upto enhances the coinductive proof method for
bisimilarity, providing efficient proof techniques for
checking properties of different kinds of systems. We prove
the soundness of such techniques in a fibrational setting,
building on the seminal work of Hermida and Jacobs. This
allows us to systematically obtain upto techniques not only
for bisimilarity but for a large class of coinductive
predicates modelled as coalgebras. By tuning the parameters of
our framework, we obtain novel techniques for unary predicates
and nominal automata, a variant of the GSOS rule format for
similarity, and a new categorical treatment of weak
bisimilarity.

201718: This fall I am teaching a TD in Algorithms for L3 students
at Paris 7. The course's webpage
is
here.

201213: As a lecturer/research associate at the University
of Leicester, I was responsible for two courses:
 Data Structures and Development Environments
(approx. 100 students, L1 level)
 Operating Systems, Networks and Distributed Systems
(approx. 70 students, L2 level)

20102011 I supervised seven MSc projects at the University of Leicester
 20112012 I supervised eight MSc projects at the
University of Leicester
 2007–2011:
I have been teaching assistant for several modules at the University of Leicester:
Java for Bioinformatics (MSc module), Program Design,
Databases and Web Applications, Software Reliability (MSc
module), Functional Programming, Logic Programming, Logic
and Problem Solving, Discrete Structures, Information
Management

I am in the Publicity committee
of ACM SIGLOG.

I have served on several Program Committes: CSL 2018, MFPS
2017, FSCD 2017, CALCO 2017, CONCUR 2016, CMCS 2016, CALCO
2015, MFPS 30 , CMCS 2014, CALCO 2013, ICE 2013, CMCS 2012

I was the Program Chair of CALCO 2017 Early Ideas affiliated Workshop

Invited talks: CMCS 2018, ALCOP 2017, CALCO 2015, MFPS 2015
(invited tutorial speaker)
Email: petrisanirif.fr
Office: 4016, Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75013 Paris
Work phone: +33 (0)1 57 27 94 00
Postal address: IRIF, Université Paris Diderot  Paris 7  Case 7014, F75205 Paris Cedex 13