MSCA project Walgo

Jean-Yves Moyen
MSCA project Walgo

E-mail: Jean-Yves.Moyen `at` lipn.univ-paris13.fr

From September 2015 to August 2017, I was a MSCA fellow funded by grant number 65522 "Walgo". Here is the list of publications and work done during that period.

Habilitation Thesis

I submitted my Habilitation thesis (Danish Doktordisputats, equivalent to the French Habilitation à Diriger des Recherches) in February 2017.
Implicit Complexity, in Theory and Practice

Equivalences between programs

Walgo focused on the study of the equivalences between programs, assuming that "implementing the same Algorithm" is such an equivalence and trying to get insights into it.

James Avery, Jean-Yves Moyen, Jakob Grue Simonsen, Pavel Růžička, Chains, Antichains, and Complements in Infinite Partition Lattices, under revision at Algebra Universalis.
Jean-Yves Moyen, Jakob Grue Simonsen, More intensional versions of Rice’s Theorem, Dice 2016 (slides).
Jean-Yves Moyen, Jakob Grue Simonsen, Computability in the Lattice of Equivalence Relations, Dice 2017 (slides).

Implicit Complexity and Compilation

I supervised the PhD. of Thomas Rubiano, working on bringing ideas from Implicit Complexity into the mainstream compiler LLVM.

Jean-Yves Moyen, Thomas Rubiano, Detection of Non-Size Increasing Programs in Compilers, Dice 2016.
Jean-Yves Moyen, Thomas Rubiano, Thomas Seiller, Loop Quasi-Invariant Chunk Motion, Dice 2017.
Jean-Yves Moyen, Thomas Rubiano, Thomas Seiller, Loop Quasi-Invariant Chunk Motion, ATVA 2017.

Formal Proofs of Implicit Complexity

We made a formal proof (in the proof assistant Coq) of my former result on Quasi-Interpretations.

Hugo Ferée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak, Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations, CPP 2018.

Miscellaneous

Some technical stuff I've done during that time frame, not directly related to Walgo but still of interest. All this is @CC BY-NC and comes with no warranty. Use at your own risk.

I wrote a LaTeX template for the MSCA application.
The EU only provides a Word template and I'm way more comfortable using LaTeX. So I made this template. Beware that it was done for the 2014 application and the template has changed since, hence you'll need to adapt it to the current application.
I toyed with Optional Contents Groups to try and implement working Hypertext proofs in LaTeX, following some ideas by Leslie Lamport on Structured proofs.
I toyed with ways to implement a truly Unicode keyboard that doesn't use long sequences of keys to input potentially tens of thousand of various characters.