Contact:
Paul[at]Brunet-Zamansky[dot]fr.
I am a Research Associate in the
Programming Principles, Logic and
Verification group (PPLV) at
UCL’s Dept. of Computer Science,
which I joined in January 2017. Since October 2018 I am a member of the
IRIS project,
working with David Pym
and
James Brotherston.
I hold a PhD in Computer Science from the University of
Lyon, under the
supervision of Damien Pous.
My research focuses on theoretical aspects
of software verification. More
specifically I study the algebraic
properties of various models of program
behaviour. My interests also include
logic, automata theory, mechanised proofs,
concurrency theory and nominal
mathematics. I have authored a number of
papers
in peer-reviewed international conferences
and journals on some of these topics.
My CV is here, and you can download it as a PDF in
english
or in french.
I have profiles on these
websites:
20 October 2020 —
I will serve on the program committee of CONCUR 2021. More info will be published on the following website:
Qonfest.
04 June 2020 —
I'll be talking about new models of concurrent Kleene algebra at the
PPS seminar on Tuesday 9 June at 4pm.
My research interests include (but are not limited
to) language theory, formal proofs, type theory, relation algebra,
automata theory...
Partially Observable Concurrent Kleene Algebra.
×
Partially Observable Concurrent Kleene Algebra.
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.
@inproceedings{brunet25-2020,
title="Partially Observable Concurrent Kleene Algebra",
author={Brunet, Paul and Docherty, Simon and Kappé, Tobias and Rot, Jurriaan and Silva, Alexandra and Wagemaker, Jana},
year={2020},
booktitle={CONCUR},
doi={"10.4230/LIPIcs.CONCUR.2020.20"},
}
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra.
×
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra.
Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protect from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for pratical purposes. We provide a logic, ‘pomset logic’, that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. We develop the basic metatheory for the relationship between pomset logic and CKA and illustrate this relationship with simple examples.
@inproceedings{brunet22-2020,
title="Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra",
author={Brunet, Paul and Pym, David},
year={2020},
booktitle={FSCD},
doi={"10.4230/LIPIcs.FSCD.2020.8"},
}
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness.
×
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness.
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditional and while-loops. It turns out integrating tests in CKA is subtle, due to their interaction with parallel threads. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO.
@inproceedings{brunet21-2020,
title="Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness",
author={Brunet, Paul and Kappé, Tobias and Silva, Alexandra and Wagemaker, Jana and Zanasi, Fabio},
year={2020},
booktitle={FoSSaCS},
doi={"10.1007/978-3-030-45231-5_20"},
}
A Complete Axiomatisation of a Fragment of Language Algebra.
×
A Complete Axiomatisation of a Fragment of Language Algebra.
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
@inproceedings{brunet20-2020,
title="A Complete Axiomatisation of a Fragment of Language Algebra",
author={Brunet, Paul},
year={2020},
booktitle={CSL},
doi={"10.4230/LIPIcs.CSL.2020.11"},
}
A note on commutative Kleene algebra.
×
A note on commutative Kleene algebra.
In this paper we present a detailed proof of an important result of algebraic logic: namely that the free commutative Kleene algebra is the space of semilinear sets. The first proof of this result was proposed by Redko in 1964, and simplified and corrected by Pilling in his 1970 thesis. However, we feel that a new account of this proof is needed now. This result has acquired a particular importance in recent years, since it is a key component in the completeness proofs of several algebraic models of concurrent computations (bi-Kleene algebra, concurrent Kleene algebra...). To that effect, we present a new proof of this result.
@techreport{brunet23-2019,
title="A note on commutative Kleene algebra",
author={Brunet, Paul},
year={2019},
institution={},
}
A Kleene theorem for nominal automata.
×
A Kleene theorem for nominal automata.
Nominal automata are a widely studied class of automata designed to recognise languages over infinite alphabets. In this paper, we present a Kleene theorem for nominal automata by providing a syntax to denote regular nominal languages. We use regular expressions with explicit binders for creation and destruction of names and pinpoint an exact property of these expressions – namely memory-finiteness – that identifies a subclass of expressions denoting exactly egular nominal languages.
@inproceedings{brunet17-2019,
title="A Kleene theorem for nominal automata",
author={Brunet, Paul and Silva, Alexandra},
year={2019},
booktitle={ICALP},
doi={"10.4230/LIPIcs.ICALP.2019.107"},
}
|
Coauthors
|
My research is the result of collaborations
with many friends and colleagues. I have in
particular written papers together with these
people:
Alexandra Silva, Damien Pous, Tobias Kappé, Fabio Zanasi, Bas Luttik, Jana Wagemaker, Jurriaan Rot, Insa Stucke, Georg Struth, Daniela Petrişan, David Pym, and Simon Docherty.
|
Phd thesis, to find out more, see
link
or
lien
.
|
I am a member of the PC of WoLLIC 2020.
I have been a subreviewer for the following conferences, workshops and journals:
MFCS, FSTTCS, JFLA, JLAMP,
EXPRESS/SOS, ICALP, FoSSaCS, Petri
Nets, ICFP, LiCS, CPP, FORTE, SoSyM,
TDSC, CSR.
- MEng/BSc Computer Science, University College London
- Computability and Complexity Theory – problem classes (2017-2019)
[More]
- Master program in ÉNS de Lyon
- Semantics and Verification – exercises (2016) [more]
- Master program in UCB Lyon 1
- Calculability and complexity – exercises (2014-2015)
- Bachelor degree in UCB Lyon 1
- Industrial Internship – reports (2014-2016)
- Theory of formal languages – exercises & project (2013-2015)
- Classical logic – exercises & project (2014-2015)
- Numeric Algorithms – exercises (2013)
- Algorithmics and Imperative programming – exercises & programming (2013-2014)