Marc Bagnol - research personal page

(teaching: this way)

I am currently a JSPS Postdoc at the University of Tokyo in the MMM group.

If you want to contact me, here's my e-mail adress:


Articles:

(conferences)

The Shuffle Quasimonad and Modules with Differentiation and Integration; (MFPS XXXII) joint work with Richard Blute, J. Robin B. Cockett and Jean-Simon Lemay,
Unary Resolution: Characterizing Ptime; (FoSSaCS 2016) joint work with Clément Aubert and Thomas Seiller.
Representation of Partial Traces; (MFPS XXXI) [slides].
MALL proof equivalence is Logspace-complete, via binary decision diagrams; (TLCA 2015) [slides].
On the dependencies of logical rules; (FoSSaCS 2015) joint work with Alexis Saurin and Amina Doumane.
Logic Programming and Logarithmic Space; (APLAS 2014) [slides] joint work with Clément Aubert, Paolo Pistone and Thomas Seiller.
Unification and Logarithmic Space; (RTA/TLCA 2014) joint work with Clément Aubert.
Analyse de dépendances et correction de réseaux de preuve; (JFLA 2014, in french) joint work with Alexis Saurin and Amina Doumane.

(journals)

MALL Proof Equivalence is Logspace-complete, via Binary Decision Trees; (to appear in LMCS)
Unification and Logarithmic Space; (to appear in LMCS) joint work with Clément Aubert.


PhD Thesis: On the Resolution Semiring

Book version in black and white, for printing.
Screen version in color, for displaying.
[Slides] of the defense.

Talks (lecture notes, abstracts, slides):

Multiplicative-Additive Proof Equivalence is Logspace-complete; (2017) the slides of a seminar I gave at the RIMS.
Representation of Partial traces; (2015) the abstract of my talk at the TACL 2015 conference.
GoI part 2: Unification and exponentials; (2013) the notes of my lecture on Geometry of Interaction at the Linear Logic summer school in Torino. Part 1 by Thomas Seiller.
Le critère de Mogbil-Naurois; (2013, in french) the notes of my lecture on the NL-complete Mogbil-Naurois criterion for proofnets at the GdT LDP.
L'algèbre d'unification; (2013, in french) the notes of my lecture on the unification algebra at the GdT LDP.
Réseaux de preuve pour MALL; (2012, in french) the notes of my lecture on proofnets for MALL at the GdT Logique.
Déduction naturelle et calcul des séquents; (2012, in french) the notes of my lecture on natural deduction and sequent calculus at the GdT Logique.

LaTeX:

pn.sty; a set of TikZ macros to draw hypergraphs and proofnets (experimental!), with some documentation.