Daniela Petrisan

About me

I am a postdoc working on Mai Gehrke's ERC project DuaLL in the Automata team of LIAFA at Université Paris Diderot - Paris 7. Before joining LIAFA, 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 fixed-term lectureship and a research associate position at the University of Leicester.

Here is a my CV.

News

Our paper Quantifiers on languages and codensity monads was accepted to LICS 2017. A long version is here.
Please consider submiting to FSCD 2017.
Please consider submiting to CALCO 2017.
I am the PC chair of the CALCO Early Ideas 2017, affiliated with CALCO 2017.

Publications (see also dblp)

In journals

A general account of coinduction up-to,
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 up-to},
   journal=[Acta Informatica},
   year={2016},
   pages={1--64},
   issn={1432-0525},
   doi={10.1007/s00236-016-0271-4},
   url={http://dx.doi.org/10.1007/s00236-016-0271-4},
   }

Bisimulation up-to 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 up-to 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 well-known 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 up-to 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.
Relation lifting, with an application to the many-valued cover modality,
M. Bílková, A. Kurz, D. Petrisan, J. Velebil, Logical Methods in Computer Science 9(4), (2013)
[link] [abstract] [bibtex]
@article{BKPV13,
   author = {Marta B\'{\i}lkov{\'a} and Alexander Kurz and Daniela Petri{\c s}an and J{\' i}{\v r}{\' i} Velebil},
   title = {Relation lifting, with an application to the many-valued cover modality},
   journal = {Logical Methods in Computer Science},
   volume = {9},
   number = {4},
   year = {2013},
   }

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.
Nominal Coalgebraic Data Types with Applications to Lambda Calculus,
A. Kurz, D. Petrisan, P. Severi, F. de Vries, Logical Methods in Computer Science 9(4), (2013)
[link] [abstract] [bibtex]
@article{KPSV13,
   author = {Alexander Kurz and Daniela Petrisan and Paula Severi and Fer-Jan de Vries},
   title = {Nominal Coalgebraic Data Types with Applications to Lambda Calculus},
   journal = {Logical Methods in Computer Science},
   volume = {9},
   number = {4},
   year = {2013},
   }

We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.
On Universal Algebra over Nominal Sets.
A. Kurz, D. Petrisan, Mathematical Structures in Computer Science, Volume 20 (2): 285-318 (2010).
[link] [abstract] [bibtex]
@article{KP10a,
   author = {Alexander Kurz and Daniela Petrisan},
   title = {On universal algebra over nominal sets},
   journal = {Mathematical Structures in Computer Science},
   volume = {20},
   number = {2},
   year = {2010},
   pages = {285-318},
   }

We investigate universal algebra over the category Nom of nominal sets. Using the fact that Nom is a full reflective subcategory of a monadic category, we obtain an HSP-like theorem for algebras over nominal sets. We isolate a "uniform" fragment of our equational logic, which corresponds to the nominal logics present in the literature. We give semantically invariant translations of theories for nominal algebra and NEL into "uniform" theories, and systematically prove HSP theorems for models of these theories.
Presenting Functors on Many-Sorted Varieties and Applications.
A. Kurz, D. Petrisan, Information and Computation. 208(12): 1421-1446 (2010)
[link] [abstract] [bibtex]
@article{KP10b,
   author = {Alexander Kurz and Daniela Petrisan},
   title = {Presenting functors on many-sorted varieties and applications},
   journal = {Inf. Comput.},
   volume = {208},
   number = {12},
   year = {2010},
   pages = {1421-1446}
   }

This paper studies several applications of the notion of a presentation of a functor by operations and equations. We show that the technically straightforward generalisation of this notion from the one-sorted to the many-sorted case has several interesting consequences. First, it can be applied to give equational logic for the binding algebras modelling abstract syntax. Second, it provides a categorical approach to algebraic semantics of first-order logic. Third, this notion links the uniform treatment of logics for coalgebras of an arbitrary type T with concrete syntax and proof systems. Analysing the many-sorted case is essential for modular completeness proofs of coalgebraic logics.

In conferences

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 well-suited for applying tools from Stone duality as applied in semantics. The main focus of the paper is the development of topo-algebraic 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 Egli-Milner type condition on generalised factorisations of ultrafilters on words.
Lax Bialgebras and Up-To Techniques for Weak Bisimulations,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CONCUR 2015
[abstract]
Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to 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 language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based 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 F-J. 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 non-termination and infinite data) and on the other hand 2-categorical (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 many-sorted 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 up-to in a fibrational setting,
F. Bonchi, D. Petrisan, D. Pous, J. Rot, CSL-LICS 2014
[link] [arxiv link] [abstract] [bibtex]
@inproceedings{DBLP:conf/csl/BonchiPPR14,,
   author = {Filippo Bonchi and Daniela Petrisan and Damien Pous and Jurriaan Rot},
   title = {Coinduction up-to in a fibrational setting},
   booktitle = {Joint Meeting of the Twenty-Third {EACSL} Annual Conference on Computer Science Logic {(CSL)} and the Twenty-Ninth Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS), {CSL-LICS} '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 up-to 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 up-to 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.
An Alpha-Corecursion Principle for the Infinitary Lambda Calculus.
A. Kurz, D. Petrisan, P. Severi, F. de Vries, CMCS 2012.
[link] [abstract] [bibtex]
@inproceedings{KPSV12,
   author = {Alexander Kurz and Daniela Petrisan and Paula Severi and Fer-Jan de Vries},
   title = {An Alpha-Corecursion Principle for the Infinitary Lambda Calculus},
   booktitle = {CMCS},
   editor = {Dirk Pattinson and Lutz Schroder},
   year = {2012},
   pages = {130-149},
   ee = {http://dx.doi.org/10.1007/978-3-642-32784-1_8},
   }

Gabbay and Pitts proved that lambda-terms up to alpha-equivalence constitute an initial algebra for a certain endofunctor on the category of nominal sets. We show that the terms of the infinitary lambda-calculus form the final coalgebra for the same functor. This allows us to give a corecursion principle for alpha-equivalence classes of finite and infinite terms. As an application, we give corecursive definitions of substitution and of infinite normal forms (Böhm, Lévy-Longo and Berarducci trees).
Stone duality for nominal Boolean algebras with `new'.
M. Gabbay, T. Litak, D. Petrisan, CALCO 2011.
[link] [abstract] [bibtex]
@inproceedings{GLP11,
   author = {Murdoch James Gabbay and Tadeusz Litak and Daniela Petrisan},
   title = {Stone Duality for Nominal Boolean Algebras with `new'},
   booktitle = {CALCO},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   volume = {6859},
   year = {2011},
   pages = {192-207},
   ee = {http://dx.doi.org/10.1007/978-3-642-22944-2_14},
   }

We define Boolean algebras over nominal sets with a function symbol И mirroring the И ‘fresh name’ quantifier (Banonas), and dual notions of nominal topology and Stone space. We prove a representation theorem over fields of nominal sets, and extend this to a Stone duality.
Relation Liftings on Preorders.
M. Bilkova, A. Kurz, D. Petrisan, J. Velebil, CALCO 2011.
[link] [abstract] [bibtex]
@inproceedings{BKPV11,
   author = {Marta B\'{\i}lkov{\'a} and Alexander Kurz and Daniela Petrisan and Jiri Velebil},
   title = {Relation Liftings on Preorders and Posets},
   booktitle = {CALCO},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   volume = {6859},
   year = {2011},
   pages = {115-129},
   ee = {http://dx.doi.org/10.1007/978-3-642-22944-2_9}
   }

The category Rel(Set) of sets and relations can be described as a category of spans and as the Kleisli category for the powerset monad. A set-functor can be lifted to a functor on Rel(Set) iff it preserves weak pullbacks. We show that these results extend to the enriched setting, if we replace sets by posets or preorders. Preservation of weak pullbacks becomes preservation of exact lax squares. As an application we present Moss’s coalgebraic over posets.
A Duality Theorem for Real C* Algebras.
A.M. Moshier, D. Petrisan, CALCO 2009.
[link] [abstract] [bibtex]
@inproceedings{MP09,
   author = {M. Andrew Moshier and Daniela Petrisan},
   title = {A Duality Theorem for Real {\it C}$^{\mbox{*}}$ Algebras},
   booktitle = {CALCO},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   volume = {5728},
   year = {2009},
   pages = {284-299},
   ee = {http://dx.doi.org/10.1007/978-3-642-03741-2_20},
   }

The full subcategory of proximity lattices equipped with some additional structure (a certain form of negation) is equivalent to the category of compact Hausdorff spaces. Using the Stone-Gelfand-Naimark duality, we know that the category of proximity lattices with negation is dually equivalent to the category of real C* algebras. The aim of this paper is to give a new proof for this duality, avoiding the construction of spaces. We prove that the category of C* algebras is equivalent to the category of skew frames with negation, which appears in the work of Moshier and Jung on the bitopological nature of Stone duality.
Functorial Coalgebraic Logic: The case of many-sorted varieties.
A. Kurz, D. Petrisan, CMCS 2008.
[link] [abstract] [bibtex]
@article{KP08,
   author = {Alexander Kurz and Daniela Petrisan},
   title = {Functorial Coalgebraic Logic: The Case of Many-sorted Varieties},
   journal = {Electr. Notes Theor. Comput. Sci.},
   volume = {203},
   number = {5},
   year = {2008},
   pages = {175-194},
   ee = {http://dx.doi.org/10.1016/j.entcs.2008.05.025},
   bibsource = {DBLP, http://dblp.uni-trier.de}
   }

Following earlier work, a modal logic for T-coalgebras is a functor L on a suitable variety. Syntax and proof system of the logic are given by presentations of the functor. This paper makes two contributions. First, a previous result characterizing those functors that have presentations is generalized from endofunctors on one-sorted varieties to functors between many-sorted varieties. This yields an equational logic for the presheaf semantics of higher-order abstract syntax. As another application, we show how the move to functors between many-sorted varieties allows to modularly combine syntax and proof systems of different logics. Second, we show how to associate to any set-functor T a complete (finitary) logic L consisting of modal operators and Boolean connectives.

Preprints

Algebraic Theories over Nominal Sets,
A. Kurz, D. Petrisan, J. Velebil.
[arxiv link] [abstract]
We investigate the foundations of a theory of algebraic data types with variable binding inside classical universal algebra. In the first part, a category-theoretic study of monads over the nominal sets of Gabbay and Pitts leads us to introduce new notions of finitary based monads and uniform monads. In a second part we spell out these notions in the language of universal algebra, show how to recover the logics of Gabbay-Mathijssen and Clouston-Pitts, and apply classical results from universal algebra.

Thesis

My PhD thesis Investigations into Algebra and Topology over Nominal Sets is available here.