%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[a4paper, 11pt]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage[utf8]{inputenc}
\usepackage{mathptmx} % Times font for text, CM font for \tt
\usepackage{bibeval}
\usepackage[bookmarks=true, bookmarksopen=true, colorlinks=true, linkcolor=blue, citecolor=blue, urlcolor=blue]{hyperref}
\usepackage{enumitem} % more compact lists
\usepackage{color, soul} % only for revisions of the template
\usepackage{xspace}
%% Nos packages, options et macros
\usepackage[T1]{fontenc}
\usepackage[centering]{geometry}
\usepackage{url, microtype, titlesec}
\usepackage{mathtools, amssymb}
\usepackage[euler-digits, euler-hat-accent]{eulervm}
\usepackage[cal=euler, scr=dutchcal, scrscaled=1.05]{mathalfa}
\usepackage{xcolor}
% titlesec
\titleformat{\paragraph}[runin]{\bfseries}{\theparagraph.}{.5em}{}[.]
\titlespacing{\paragraph}{0em}{0.5\baselineskip}{0.5em}[]
\setlist{nolistsep}
\textwidth15cm
\textheight24cm
\topmargin-1.5cm
\newcommand{\theme}{Proofs and Verification}
\newcommand{\project}{$\pi r^2$}
\newcommand{\evaldate}{March 2019} % date of evaluation seminar
\newcommand{\prevevaldate}{March 2015} % date of previous eval seminar or project creation date
\def\Equations{\textsc{Equations}\xspace}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Nos commandes
\newcommand{\yves}[1]{\textcolor{orange}{Yves~: #1}}
\newcommand{\yann}[1]{\textcolor{orange}{Yann~: #1}}
\newcommand{\ms}[1]{\textcolor{orange}{Matthieu~: #1}}
\newcommand{\plc}[1]{\textcolor{orange}{PL~: #1}}
\newcommand{\hugo}[1]{\textcolor{orange}{Hugo~: #1}}
\newcommand{\alexis}[1]{\textcolor{orange}{Alexis~: #1}}
\newcommand{\afaire}[1]{\textcolor{red}{À faire~: #1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{center}
{\Large Evaluation of Inria theme \theme \par}
\vspace*{2em}
{\LARGE Project-team \project \par}
\vspace*{2em}
{\large \evaldate \par}
\end{center}
\bigskip
%{\footnotesize\sl Guidelines are in footnotesize format. XX are to be
%replaced by the appropriate name or number. TBR means that you have to
%remove this comment in the final version of the document, it is just a
%guideline. TBR}
%
%{\footnotesize\sl {\bf Overall document and subsection lengths}: We give indications below of the expected appproximate length for each subsection. Those indications are to be understood as crude guidelines, not strict limitations. However, the overall document length should not be longer than 40 pages (excluding the bibliography section). TBR}
\subsection*{Project-team title: Design, study and implementation of languages for proofs and programs}
\subsection*{Scientific leader: Pierre-Louis Curien}
\subsection*{Research centers: Paris}
\subsection*{Common project-team with: CNRS, Université Paris~7}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Personnel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Current composition of the project-team:}
Research scientists and faculty members:
\begin{itemize}
\item Thierry Coquand, Prof. University of Gothenburg (INRIA chair)
\item Pierre-Louis Curien, DR CNRS (team leader)
\item Yves Guiraud, CR INRIA
\item Hugo Herbelin, DR INRIA
\item Pierre Letouzey, MCF Université Paris~7
\item Jean-Jacques Lévy, DR INRIA (emeritus)
\item Yann Régis-Gianas, MCF Université Paris~7
\item Alexis Saurin, CR CNRS
\item Matthieu Sozeau, CR INRIA
\end{itemize}
Engineers:
\begin{itemize}
\item Daniel de Rauglaudre, IR INRIA
\item Thierry Martinez, IR INRIA (part-time)
\end{itemize}
Postdocs:
\begin{itemize}
\item Eric Finster, INRIA (until Feb.~2019)
\item Kailiang Ji, INRIA (until Feb.~2019)
\item Exequiel Rivas, INRIA (until Feb.~2019)
\end{itemize}
Ph.D.~students:
\begin{itemize}
\item Antoine Allioux, INRIA (from Feb.~2018)
\item Ahbishek De, FSMP (from Sep.~2018)
\item Cédric Ho Thanh, Université Paris~7 (from Sep.~2017)
\item Théo Zimmermann, Université Paris~7 (from Sep.~2016)
\end{itemize}
Administrative assistant:
\begin{itemize}
\item Mathieu Mourey, INRIA (from Sep.~2018)
\item Sandrine Verges, INRIA (until June~2018)
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Personnel at the start of the evaluation period (\prevevaldate)}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|} \hline
& INRIA & CNRS & University & Other & {\bf Total} \\ \hline \hline
DR (1) / Professors
& 1 & 1 & & & {\bf 2} \\ \hline
DR emeritus
& 1 & & & & {\bf 1} \\ \hline
CR (2) / Assistant professors
& 2 & 1 & 2 & & {\bf 5} \\ \hline
%ARP and SRP (3)
% & & & & & {\bf} \\ \hline
Permanent engineers (3)
& & & & & {\bf} \\ \hline
%Temporary engineers (5)
% & & & & & {\bf} \\ \hline
Postdocs
& 1 & & & & {\bf 1} \\ \hline
PhD Students
& & & 10 & & {\bf 10} \\ \hline
{\bf Total}
&{\bf 5} &{\bf 2} &{\bf 12} & {\bf} & {\bf 19} \\ \hline
\end{tabular}
\end{center}
(1) ``Senior Research Scientist (Directeur de Recherche)''
(2) ``Junior Research Scientist (Chargé de Recherche)''
%(3) ``Inria Advanced Research Position'' and ``Inria Starting Research
%Position''
(3) ``Civil servant (CNRS, INRIA, ...)''
%(5) ``Associated with a contract (Ingénieur Expert, Ingénieur ADT,
%\ldots)''
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Personnel at the time of the evaluation (\evaldate)}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|} \hline
& INRIA & CNRS & University & Other & {\bf Total} \\ \hline \hline
DR / Professors
& 1 & 1 & & & {\bf 2} \\ \hline
DR emeritus
& 1 & & & & {\bf 1} \\ \hline
CR / Assistant professors
& 2 & 1 & 2 & & {\bf 5} \\ \hline
%ARP and SRP
% & & & & & {\bf} \\ \hline
Permanent engineers
& 1 & & & & {\bf 1} \\ \hline
%Temporary engineers
% & & & & & {\bf} \\ \hline
Post-docs
& & & & & {\bf} \\ \hline
PhD Students
& 1 & & 2 & 1 & {\bf 4} \\ \hline
{\bf Total}
&{\bf 6} &{\bf 2} &{\bf 4} & {\bf 1} & {\bf 13} \\ \hline
\end{tabular}
\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Changes in the scientific staff}
% {\footnotesize\sl Number of scientists (DR, CR, Professors, Assistant professors, ARP, SRP) that joined or left the project-team during the last four years period or since the project creation. Engineers, post-docs and PhD students are not counted. TBR.}
%\begin{center}
%\begin{tabular}{|c|c|c|c|c|c|} \hline
%DR / Professors / ARP
% & INRIA & CNRS & University & Other & {\bf Total} \\
%CR / Assistant Professors / SRP
% & & & & & {\bf} \\ \hline\hline
%Arrivals
% & & & & & {\bf} \\ \hline
%Departures
% & & & & & {\bf} \\ \hline
%\end{tabular}
%\end{center}
%
%\paragraph{Comments}
The team composition in permanent research scientists and faculty members has been stable over the period. Daniel de Rauglaudre has joined as full time INRIA research engineer in June~2015.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Current position of former project-team members}
% {\footnotesize\sl Provide a list of former project-team members, including engineers, post-docs and PhD students, who left the project-team during the evaluation period. Give name, former position in the team, current position, current employer (name and location). TBR. }
\begin{itemize}
\item Cyrille Chenavier (PhD 2013-2016), currently postdoc at INRIA Lille
\item Guillaume Claret (PhD 2012-2018), currently engineer at BlaBlaCar
\item Amina Doumane (PhD 2014-2017), currently postdoc at Warsaw University
\item Thibaut Girka (PhD 2015-2018), currently looking for a position
\item Lourdes del Carmen González Huesca (PhD 2011-2015), currently teaching assistant at University of Mexico
\item Guilhem Jaber (Postdoc ANR RAPIDO, 2016-2017), currently assistant professor at the University of Nantes
\item Matej Košic (engineer funded by ADT Coq, 2015-2016), then with the Marelle team in 2016-2017
\item Marc Lasson (Postdoc INRIA 2014-2015), currently engineer at Lexifi
\item Gabriel Lewertowski (PhD 2015-2016), currently engineer at TrustInSoft
\item Maxime Lucas (PhD 2014-2017), currently postdoc at INRIA Nantes
\item Cyprien Mangin (PhD 2015-2018), currently engineer at Google Paris
\item Étienne Miquey (PhD 2014-2017), currently postdoc at INRIA Nantes
\item Jovana Obradović (PhD 2014-2017), currently postdoc at the Institute of Mathematics of the Czech Academy of Sciences, Prague
\item Ludovic Patey (PhD 2012-2016), currently CR CNRS at Université Lyon~1
\item Pierre-Marie Pédrot (PhD 2012-2015), currently CR INRIA at INRIA Nantes
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Last INRIA enlistments}
% {\footnotesize\sl Provide a list of INRIA researchers who have been hired in the project-team including name, year of recruitment and position (CR2, CR1, DR2, DR1, ARP, SRP). TBR.}
\begin{itemize}
\item Daniel de Rauglaudre, IR2, 2015 (internal transfer from INRIA Rocquencourt)
\item Jean-Jacques Lévy, DR0 emeritus, 2014 (transfer from INRIA Saclay)
\item Yves Guiraud, CR1, 2012 (transfer from INRIA Nancy), now CRCN
\item Matthieu Sozeau, CR2, 2010 (hiring), now CRCN
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{Other comments:}
% {\footnotesize\sl State in this section any modification relevant to the project-team such as a change of the scientific leader or any other information you would like to add. TBR.}
The team will reach its planned end-date at the end of 2019, when the current scientific leader will retire. The team members are currently working on the collective scientific plans after that date.
Amina Doumane's PhD thesis (defended in June 2017) received the EACSL Ackermann award as well as Prix Gilles Kahn, attributed by the SIF. She also received the Kleene award
of the best student paper at LICS 2017, as well as the ``Prix scientifique de {\it La Recherche}'' 2017 for the best French scientific paper in computer science.
Étienne Miquey received the Kleene award
of the best student paper at LICS 2018. He also received the prize of the best thesis in mathematcis of Uruguay in 2018.
Matthieu Sozeau, together with Nicolas Tabareau (Inria Nantes) and Eric Tanter (Univ.\ Chile in Santiago) received the Distinguished Paper Award at
ICFP 2018.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Research goals and results}\label{sec:Research}
%{\footnotesize\sl A double length constraint here: the description of the research axes below should be max 3 pages per axis and the global size of section \ref{sec:Research} should be at most 16 pages. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Keywords}
% {\footnotesize\sl Feel free to reuse the keywords from the yearly activity reports. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Proof theory, proof assistants, Coq, types, type theory, dependent types, intuitionistic, classical, and linear logic, control operators, delimited control, programming languages, dependently typed programming languages, effects, fixed-point logics, induction and coinduction, rewriting, polygraphs, higher categories, higher algebra, operas, homotopy.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Context and overall goals of the project}
% {\footnotesize\sl Develop a structured view of the research program rather than simply presenting a set of ideas to be explored. Recommended length: 1 page; maximal length: 2 pages. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The $\pi r^2$ team studies the foundational aspects of formal proofs
and programs, and develops the Coq proof assistant software -- hosting
the current coordinator of the development team --, with a focus on
the dependently-typed programming language aspects of Coq. Since 2012,
the team has also extended its scope to the effective aspects of
higher algebra, which shares foundational tools with
recent advances in type theory.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Proof theory and the Curry-Howard correspondence}
Proof theory is the branch of logic devoted to the study of the
structure of proofs. A significant early contributor to this field is
Gentzen, who developed in 1935 two logical formalisms
that are now central to the study of proofs~\footcite{Gentzen35}. These are
natural deduction, that is particularly well-suited to
simulate the intuitive notion of reasoning, and
sequent calculus, a syntax with deep geometrical
properties that is particularly well-suited for proof automation.
%
Proof theory gained a remarkable importance in computer science when
it became clear, after genuine observations first by
Curry~\footcite{Curry34,Curry58}, then later by Howard and de Bruijn
at the end of the 60's~\footcite{Howard80,deBruijn68}, that proofs had
the very same structure as programs: for instance, natural deduction
proofs can be identified as programs of the typed
$\lambda$-calculus. An
%This correspondence extended an earlier,
asymmetrical assignment of programs to proofs, named realisability, had been developed earlier by Kleene~\footcite{Kleene45},
Gödel~\footcite{Godel58} and Kreisel~\footcite{Kreisel59} around the
ideas of Brouwer. Altogether, realisability and the Curry-Howard
correspondence between proofs and typed programs have been the
starting point to a large spectrum of researches and results
contributing to deeply connect logic and computer science.
The idea that proofs have computational contents has for long been
limited to the intuitionistic case, until it was discovered in 1990
by Griffin~\footcite{Griffin90} that this connection was extensible to
classical logic, proividing a stimulus for
exploring new correspondences between computer science and logic. One of
these, explored by Herbelin and
Curien~\footcite{Herbelin94,CurienHerbelin00},
%and important for us,
was the computational understanding of Gentzen's sequent calculus,
which not only makes a bridge with abstract machines in programming
but also highlights symmetries between a program and its evaluation
context, as well as between the standard notions of call-by-name and
call-by-value evaluation semantics. Other explorations include: the question of the computational content of
the classical axiom of choice, connecting it in particular to lazy
evaluation and coinduction~\footcite{Herbelin12}; that of the
computational content of the forcing method, connecting it to memory
assignment; that of organising the computational content of
connectives around concepts such as polarity and focusing.
\subsubsection{Type Theory, development of Coq, and further research around proofs and programs}
In 1971, Martin-Löf introduced a formalism, referred to as modern type
theory, that is both a logical system and a typed functional programming
language. The Calculus of Constructions was then
designed in 1985 by Coquand and Huet~\footcite{Coquand85,CoqHuet85a}, based on Girard-Reynolds System F.
This system served as the foundation of
the first implementation of Coq in 1984. In~1989, Coquand and
Paulin~\footcite{CoqPau89} designed an extension of the Calculus of
Constructions with a generalisation of algebraic datatypes called
inductive types, leading to the Calculus of Inductive Constructions
(CIC) that started to serve as a new foundation for Coq, which had its
first public release, and is still at the core of the current system
\cite{coqdevelopmentteam:hal-01954564}.
Over the course of 30 years of development, Coq has turned into a
reference proof assistant, for the formalisation of mathematics and
computer systems. The main ingredients of Coq are:
\begin{itemize}
\item A relatively small kernel, following the de Bruijn principle.
Today, the kernel is essentially a type checker for the Polymorphic
Calculus of Cumulative Inductive Constructions: it includes a standard
dependent type theory, with universe polymorphism and cumulativity,
mutual inductive and coinductive families, (co-)recursive definitions
and case analysis. Additionally, the kernel
includes efficient reduction machines for testing definitional
equality of terms and a module system.
\item A high-level language (Gallina) that can be elaborated down to the
kernel, by means of a type inference algorithm relying on higher-order
unification and a pattern-matching compiler, coercions, overloading
mechanisms and notations.
\item An interactive proof engine allowing to prove theorems by
gradually refining a set of goals using various tactics and decision
procedures.
% Proof scripts are written using a
% tactic language. There is a large set of built-in tactics available,
% from the application of basic rules of the calculus to automated
% decision procedures for various theories (e.g.\ rings, linear
% arithmetic...). Complex tactics can be programmed using the very
% liberal Ltac scripting language or directly in Gallina, using the
% reflection methodology to ensure their correctness.
\item A set of libraries developing standard structures such as numbers,
lists, finite sets and maps along with standard theories of sets,
relations and orders.
\item A toplevel system based on a state transition machine allowing to
process proofs asynchronously, which is used by the CoqIDE GUI.
\item An extraction procedure that maps programs (or even computational
proofs) of the CIC to functional programs.
\end{itemize}
\medskip
Our research in this broad field targets the following main aspects:
\begin{itemize}
\item[-] The study and implementation of extended type theories, refining
and providing more expressivity to the core calculus: this covers work on
proof-irrelevance, the treatment of universes and the integration of
concepts from homotopy type theory and proof theory such as the
treatment of equality or effects in the system.
\item[-] Dependently-typed programming and proving: manipulation of
dependently-typed structures in programs and proofs poses some
theoretical and practical challenges. Our goal here is to provide
high-level tools for the development of dependently-typed
programs, their verification and efficient compilation.
\item[-] Since the last evaluation in 2015, we also developed two research directions: one is the study of infinitary proof systems, and the other is laying foundations for incremental programming, for which more details are provided in Sections~\ref{Research-axis-2} and~\ref{Research-axis-4}, respectively.
\end{itemize}
% \paragraph{Towards the calculus of constructions}
% The $\lambda$-calculus, defined by Church~\footcite{Church32}, is a
% remarkably succinct model of computation that is defined via only
% three constructions (abstraction of a program with respect to one of
% its parameters, reference to such a parameter, application of a program
% to an argument) and one reduction rule (substitution of the formal
% parameter of a program by its effective argument). The
% $\lambda$-calculus, which is Turing-complete, i.e.\ which has the same
% expressiveness as a Turing machine (there is for instance an encoding of
% numbers as functions in $\lambda$-calculus), comes with two possible
% semantics referred to as call-by-name and call-by-value evaluations.
% Of these two semantics, the first one, which is the simplest to
% characterise, has been deeply studied in the last
% decades~\footcite{Barendregt84}.
% %
% For explaining the Curry-Howard correspondence, it is important to
% distinguish between intuitionistic and classical logic: following
% Brouwer at the beginning of the 20$^{\mbox{\scriptsize th}}$ century,
% classical logic is a logic that accepts the use of reasoning by
% contradiction while intuitionistic logic proscribes it. Then,
% Howard's observation is that the proofs of the intuitionistic natural
% deduction formalism exactly coincide with
% programs in the (simply typed) $\lambda$-calculus.
% %
% A major achievement has been accomplished by Martin-Löf who designed in
% 1971 a formalism, referred to as modern type theory, that was both a
% logical system and a (typed) programming language~\footcite{MartinLof71}.
% %
% In 1985, Coquand and Huet~\footcite{Coquand85,CoqHue85a} in the Formel
% team of INRIA Rocquencourt explored an alternative approach
% based on Girard-Reynolds' system
% $F$~\footcite{Girard71,Reynolds74}. This formalism, called the
% Calculus of Constructions, served as logical foundation of the first
% implementation of Coq in 1984. Coq was called CoC at this time.
% \paragraph{The Calculus of Inductive Constructions}
% The first public release of CoC dates back to 1989. The same
% project-team developed the programming language Caml (nowadays called OCaml and coordinated by the Gallium team) that
% provided the expressive and powerful concept of algebraic data types
% (a paragon of it being the type of list). In CoC, it was possible to simulate algebraic data types, but only through a
% not-so-natural not-so-convenient encoding.
% %
% In 1989, Coquand and Paulin~\footcite{CoqPau89} designed an extension of
% the Calculus of Constructions with a generalisation of algebraic
% types called inductive types, leading to the Calculus of Inductive
% Constructions (CIC) that started to serve as a new foundation for the
% Coq system. This new system, which got its current definitive name
% Coq, was released in 1991.
% %
% In practice, the Calculus of Inductive Constructions derives its
% strength from being both a logic powerful enough to formalise all common
% mathematics (as set theory is) and an expressive richly-typed
% functional programming language (like ML but with a richer type
% system, no effects and no non-terminating functions).
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \subsubsection{The development of Coq}
% From 1984 to 2009, year of creation of the team, about 40 persons have
% contributed to the development of
% Coq, out of which seven persons have contributed to bring the system to
% the place it is now. First Thierry Coquand through his foundational
% theoretical ideas, then Gérard Huet who developed the first prototypes
% with Thierry Coquand and who headed the Coq group until 1998,
% then Christine Paulin who was the main actor of the system based on
% the CIC and who headed the development group from 1998 to 2006. On the
% programming side, important steps were made by Chet Murthy who raised
% Coq from the prototypical state to a reasonably scalable system, Jean-Christophe
% Filli\^atre who turned to concrete the concept of a small trustful
% certification kernel on which an arbitrary large system can be set up,
% Bruno Barras and Hugo Herbelin who, among other extensions,
% reorganised Coq on a new smoother
% and more uniform basis able to support a new round of extensions for
% the next decade.
% The development started from the Formel team at Rocquencourt but,
% after Christine Paulin got a position in Lyon, it spread to École
% Normale Supérieure de Lyon. Then, the task force there globally
% moved to the University of Orsay when Christine Paulin got a new position there.
% On the Rocquencourt side, the part of Formel involved in ML
% moved to the Cristal team (now Gallium) and Formel got renamed into
% Coq. Gérard Huet left the team and Christine Paulin started to head a
% Coq team bilocalised at Rocquencourt and Orsay. Gilles Dowek became the
% head of the team which was renamed into LogiCal. Following Gilles
% Dowek who got a position at École Polytechnique, LogiCal
% moved to the new INRIA Saclay research center. It then
% split again, giving birth to ProVal. At the same time, the Marelle team
% (formerly Lemme, formerly Croap) which has been a long partner of the
% Formel team, invested more and more energy in both the formalisation of
% mathematics in Coq and in user interfaces for Coq.
% After various other spreadings resulting from where the wind pushed
% former PhD students, the development of Coq got
% multi-site with the development now realised by employees of INRIA, the
% CNAM and Université Paris Diderot.
% We next briefly describe the main components of Coq.
% \paragraph{The underlying logic and the verification kernel}
% The architecture adopts the so-called de Bruijn principle: the well-delimited {\em kernel}
% of Coq ensures the correctness
% of the proofs validated by the system. The kernel is rather stable
% with modifications tied to the evolution of the underlying Calculus of
% Inductive Constructions formalism. The kernel includes an
% interpreter of the programs expressible in the CIC and this
% interpreter exists in two flavours: a customisable lazy evaluation
% machine written in OCaml and a call-by-value bytecode interpreter
% written in C dedicated to efficient computations. The kernel also
% provides a module system.
% \paragraph{Programming and specification languages}
% The concrete user language of Coq, called {\em Gallina}, is a
% high-level language built on top of the CIC. It includes a type
% inference algorithm, definitions by complex pattern-matching, implicit
% arguments, mathematical notations and various other high-level
% language features. This high-level language serves both for the
% development of programs and for the formalisation of mathematical
% theories. Coq also provides a large set of commands. Gallina and
% the commands together forms the {\em Vernacular} language of Coq.
% \paragraph{Libraries} Libraries are written in the vernacular language of Coq.
% There are libraries for various arithmetical structures and various
% implementations of numbers (Peano numbers, implementation of
% $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ with binary digits, implementation
% of $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$ using machine words,
% axiomatisation of $\mathbb{R}$). There are libraries for lists, list of a specified length,
% sorts, and for various implementations of finite maps and finite sets. There
% are libraries on relations, sets, orders.
% \paragraph{Tactics} The tactics are the methods available to conduct
% proofs. This includes the basic inference rules of the CIC, various
% advanced higher level inference rules and all the automation
% tactics. Regarding automation, there are tactics for solving systems of
% equations, for simplifying ring or field expressions, for arbitrary
% proof search, for semi-decidability of first-order logic and so on.
% There is also a powerful and popular untyped scripting language for
% combining tactics into more complex tactics.
% %
% Note that all tactics of Coq produce proof certificates that are
% checked by the kernel of Coq. As a consequence, possible bugs in proof methods
% do not hinder the confidence in the correctness of the Coq
% checker. Note also that the CIC being a programming language, tactics
% can be written (and certified) in the own language of Coq if needed.
% \paragraph{Extraction} Extraction is a component of Coq that maps programs
% (or even computational proofs) of the CIC to functional programs (in
% OCaml, Scheme or Haskell). Especially, a program certified by Coq can
% further be extracted to a program of a full-fledged programming
% language then benefiting of the efficient compilation, linking tools,
% profiling tools, etc.\ of the target software.
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \subsubsection{Dependently typed programming languages}
% Dependently typed programming (shortly DTP) is an emerging concept
% referring to the diffuse and broadening tendency to develop
% programming languages with type systems able to express program
% properties finer than the usual information of simply belonging to
% specific data-types. The type systems of dependently-typed programming
% languages allow to express properties {\em dependent} of the input and
% the output of the program (for instance
% that a sorting program returns a list of same size as its
% argument). Typical examples of such languages were the Cayenne
% language, developed in the late 90's at Chalmers University in Sweden
% and the DML language developed at Boston. Since then, various new
% tools have been proposed, either as typed programming languages whose
% types embed equalities ($\Omega$mega at Portland, ATS at Boston, etc.)\
% or as hybrid logic/programming frameworks (Agda at Chalmers, Twelf at Carnegie,
% Delphin at Yale, OpTT at Univ.~Iowa, Epigram at Nottingham, etc.).
% %
% DTP contributes to a general movement leading to the fusion between
% logic and programming. Coq, whose language is both a logic and a
% programming language which moreover can be extracted to pure ML code
% plays a role in this movement and some frameworks for DTP have been
% proposed on top of Coq (Concoqtion at Rice and Colorado, Ynot at
% Harvard, Why in the ProVal team at INRIA). It also connects to Hoare logic, providing
% frameworks where pre- and post-conditions of programs are tied with
% the programs.
% %\subsubsection{Issues regarding dependently typed programming}
% DTP approached from the programming language side generally benefits
% of a full-fledged language (e.g.\ supporting effects) with efficient
% compilation. DTP approached from the logic side generally benefits of
% an expressive specification logic and of proof methods so as to
% certify the specifications. The weakness of the approach from logic
% however is generally the weak support for effects or partial
% functions.
% \paragraph{Type-checking and proof automation}
% In between the decidable type systems of conventional data-types based
% programming languages and the full expressiveness of logically
% undecidable formulae, an active field of research explores a spectrum
% of decidable or semi-decidable type systems for possible use in
% dependently typed programming languages. At the beginning of the spectrum,
% this includes, for instance, the system F's extension ML$_F$ of the ML
% type system or the generalisation of abstract data types with type
% constraints (G.A.D.T.) such as found in the Haskell programming
% language. At the other side of the spectrum, one finds
% arbitrary complex type specification languages (e.g.\ that a sorting
% function returns a list of type ``sorted list'') for which more or
% less powerful proof automation tools exist -- generally first-order ones.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Effective higher algebra}
Higher structures originate in algebraic topology, where $\infty$-groupoids have been introduced to subsume the homotopy groups of a topological space~$X$: the \emph{fundamental $\infty$-groupoid} of~$X$ has the elements of~$X$ as $0$-dimensional cells, the continuous paths of~$X$ as $1$-cells, the homotopies between continuous paths as $2$-cells, and so on.
In the last decades, higher structures have appeared in other fields of mathematics, with the study of higher-dimensional versions of classical algebraic objects (e.g.\ in mathematical physics), or of weakened versions where equations hold only up to coherent equivalences (e.g.\ in representation theory).
Recently, higher algebra has reached logic, leading to homotopy type theory (HoTT), when it was observed that the identity types are naturally equiped with a structure of $\infty$-groupoid: the $1$-cells are the proofs of equality between two terms, the $2$-cells are the proofs of equality between proofs of equality, and so on~\footcite{hottbook}.
However, higher structures are extremely complex objects, requiring new tools to reason about and to compute with them.
In order to describe higher categories combinatorially, \emph{polygraphs} have been introduced as higher generalisations of presentations by generators and relations~\footcite{Street76,Burroni93}. Polygraphs led to a theory of higher rewriting, unifying usual rewriting-like paradigms, like abstract, word and term rewriting~\footcite{Lafont03,Malbos04,Guiraud04,Guiraud06jpaa}.
%, Petri nets~\footcite{Guiraud06tcs}, or formal proofs~\footcite{Guiraud06apal}.
Specific methods have been introduced to analyse the computational properties of polygraphs, based on algebraic concepts such as derivations to prove termination, which in turn gave new tools for complexity analysis~\footcite{BonfanteGuiraud09}.
Also, polygraphs allowed the generalisation of works by Anick~\footcite{Anick86} and Squier~\footcite{Squier87,Squier94}, who computed homological and homotopical invariants of algebras and monoids by rewriting techniques. Since then, a deeper unified theory relating rewriting and homotopical algebra was established~\footcite{GuiraudMalbos09, GuiraudMalbos11, GuiraudMalbos12, GuiraudMalbos12mscs}, yielding new rewriting methods in algebra. For example, rewriting algorithms can compute a coherent presentation of a monoid~$M$, which is a combinatorial object that contains a presentation of~$M$ by generators and relations, together with higher cells that classify the different proofs of the same equalities: this is, in essence, the same as the proofs of equality of proofs of equality in homotopy type theory. When this process of ``unfolding'' proofs of equalities is pursued in every dimension, one gets a \emph{polygraphic resolution} of~$M$~\footcite{Metayer03, LafontMetayerWorytkiewicz10, AraMetayer11,GuiraudMalbos12}, which is a candidate to be a faithful formalisation of~$M$ in homotopy type theory.
\medskip
Our research in this field targets the following aspects:
\begin{itemize}
\item[-] The development of formal representations of higher structures, including syntaxes to describe them and rewriting-like tools to compute normal forms.
\item[-] The application of rewriting methods to solve various problems about higher structures, such as the computation of coherence conditions or of resolutions, especially polygraphic resolutions.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Research axis 1: Proof theory, program semantics, side effects} \label{Research-axis-1}
% {\footnotesize\sl There should be one such subsection for each main research axis of the project-team during the evaluation period. Each subsection should be approximatively 3 pages long. The number of main research axes (and therefore of such subsections) is expected to be less than 5, typically 3. For each subsection, fill the following subsubsections when appropriate. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Personnel}
% {\footnotesize\sl List the team members involved in this line of research (1-2 lines). TBR.}
Permanent members: Pierre-Louis Curien, Hugo Herbelin, Yann Régis-Gianas, Matthieu Sozeau. Postdoc: Exequiel Rivas Gadda. PhD students: Etienne Miquey, Ludovic Patey, Pierre-Marie Pédrot. Interns: Charlotte Barot, Kostia Chardonnet. External collaborator: Arnaud Spiwack (Tweag~I/O).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Project-team positioning}
% {\footnotesize\sl Should be about half a page. Positioning of the project wrt the state of the art and with regards to other INRIA project-teams and other national/international research groups (peer or competitor groups). TBR.}
This research axis is about the study of side effects in different contexts: of programming languages using general abstract notions of
side effects such as monads, arrows or applicative functors; of program certification, to validate properties of
effectful programs; of the proof-as-program
correspondence, connecting side effects to logical translations,
interpreting standard axioms as programs with side effects. Sometimes,
to compare the logical or computational strength of logical
statements, reverse mathematics may also be used.
There are presently active international research efforts on on all these aspects.
Research groups covering the first one, besides $\pi r^2$ and non-$\pi
r^2$ members of IRIF (Melliès, Ehrhard, Kesner) can be
found e.g.\ in Birmingham (Levy, Zeilberger), Edinburgh (Plotkin), in Glasgow (McBride), Ljubliana (Simpson, Pretnar), Tallinn university (Uustalu), and within the Haskell community. For the second aspect, let us mention
all groups working on the formalisation of program properties,
such as the DeepSpec group in Yale (Shao), Princeton (Appel), U. Penn
(Pierce, Weirich), MIT (Chlipala), Saarbrücken (Dreyer), Copenhagen
(Birkedal),... The study of side effects at the junction of proofs
and programs somehow stems from our team and from other members from
IRIF.
At INRIA, the Focus team includes works on general notions of
computation (e.g.~\footcite{LagoGavazzoLevy17}) but with a focus on
distributed systems. The Toccata team is about formal verification of
program properties, but with a focus on softwares for proving
properties of programs in specific programming languages. The
Gallinette team is also studying effects at the junction between
proofs and programs. Deducteam is studying proof theory with a focus
on dependent type theory, rewriting, interoperability and proof
assistants (see Section~\ref{axis:Coq}).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Scientific achievements}
%{\footnotesize\sl Describe the main contributions in 1 page. Emphasize their originality, significance and impact. Refer to the main results: publications, theses, software. TBR.}
%The results presented in this section address several kinds of
%questions.
We organise the description of our achievements along the four research contexts mentioned
in the positioning section.
\paragraph{Semantics of side effects and realisability}
We include in this section works studying the general properties of
side effects. In a large sense including classical realisability as an
effectful kind of realisability, we also include a work on an
algebraic description of classical realisability.
\medskip
\noindent{\it A theory of effects and resources}.
In joint work with Marcelo Fiore and Guillaume Munch,
Pierre-Louis Curien considered the Curry-Howard-Lambek correspondence
for effectful computation and resource management, specifically
proposing polarised calculi together with presheaf-enriched adjunction
models as the starting point for a comprehensive semantic theory
relating logical systems, typed calculi, and categorical models in
this context~\cite{curien:hal-01256092}.
\medskip
\noindent{\it Interfaces for computational effects}.
Exequiel Rivas studied the relation between interfaces for
computational effects in programming languages: arrows, idioms and
monads. Building on previous results of Lindley, Yallop and Wadler, a
categorical account was developed by means of monoidal
adjunctions (work presented at MSFP
2018~\cite{rivas:hal-01946996} and at SYCO I).
%Together with Ruben Pieters and Tom Schrijvers, a journal version including previous work on
%non-monadic handlers is ongoing.
\medskip
\noindent{\it Monads with merging}.
In collaboration with Mauro Jaskelioff, Exequiel Rivas developed
monads with merge-like operators. These operators are based on two
well-known algebraic theories for concurrency: classic process
algebras and the more recent concurrent monoids (work submitted).
%This resulted in an
%article submitted to FoSSaCS.
\medskip
\noindent{\it Relative effects: coherence for skew structures}.
In joint work with Mauro Jaskelioff, Tarmo Uustalu and Niccolò
Veltri, Exequiel Rivas developed coherence theorems in the setting
of categories with skew structures: skew monoidal categories, skew
near-rig categories, skew semigroup categories. These skew
structures are motivated by the study of relative effects in
programming languages, where the primary example is provided by relative
monads. The results are formalised in the programming language
Agda. A journal article is currently being written.
\medskip
\noindent{\it Classical realisability and implicative algebras}.
Étienne Miquey has been working with Alexandre Miquel in Montevideo on the
topic of implicative algebras. Implicative algebras are an algebraisation of
the structure needed to develop a realisability model.
%In particular, they give rise to the usual ordered combinatory algebras
%and thus to the triposes used to model classical realisability.
%An implicative algebra is given by an implicative structure (which consists
%of a complete semi-lattice with a binary operation $\rightarrow$) together
%with a separator containing the element interpreted as true in the structure.
Following the work of Munch on focalisation and
classical realisability, during his postdoc in Nantes, Étienne Miquey gave alternative
presentations within structures based on other connectives rather than
$\rightarrow$, as was originally done by Miquel. This means
disjunctive algebras (based on negation, ``par'') and conjunctive
algebras (negation, tensor) (work formalised in Coq and
presented at ITP 2018).
%% Such connectives correspond to the decomposition of the arrow
%% according to the strategy of evaluation (call-by-name/call-by-value).
%% In particular, he showed that disjunctive algebras were particular
%% cases of implicative algebras; and that conjunctive algebras can be
%% obtained by duality from disjunctive algebras. Besides, Étienne
%% Miquey has formalised the theory of implicative algebras
%% (resp. disjunctive, conjunctive) in Coq.
\paragraph{Certified effectful programming}
Monadic constructions to reason about side effects as well as type
systems to control the use of resources (which themselves can actually
be seen as side effects) have been applied to programming in Haskell
and Coq.
%We list here our results.
%\medskip
%\noindent{\em Programming with linear types}.
%Arnaud Spiwack, in collaboration with Jean-Philippe Bernardy, Mathieu
%Boespflug, Ryan R. Newton and Simon Peyton-Jones, developed an
%extension of the type system of Haskell with linear types
%\cite{bernardy:hal-01673536}. The work was presented
%at POPL 2018.
\medskip
\noindent{\em Programming with effects in Coq}.
%As part of his PhD thesis,
Guillaume Claret defined a notion of
effectful interactive computation as an embedded DSL in Coq (in the
spirit of the works on algebraic effects), and used it to implement a
web server. It is equipped with a dual notion of effectful interactive
execution context. Using these two notions together, Guillaume Claret
was able to specify and reason about interactive programs inside
Coq (work presented in ~\cite{claret:hal-01255107} and in his PhD
manuscript).
\medskip
\noindent{\em Proof techniques for effectful programming in Coq}.
In collaboration with Thomas Letan (Agence Nationale pour la Sécurité
des Systèmes Informatiques), Yann Régis-Gianas studied how free monads
can be used to develop modular implementations and proofs of effectful
systems. This proof technique is applied to the formal study of
architectural attacks on IBM PC like architectures. In collaboration
with Thomas Letan, Pierre Chifflier (ANSSI) and Guillaume Hiet (Centrale
Supélec), Yann Régis-Gianas developed a new modular approach to model
and verify effectful systems in Coq (work presented at
FM 2018).
\paragraph{Investigations in the proof-as-program correspondence}
Various investigations into relating or combining concepts from
programming with concepts from logic have been carried out.
%We list our results.
\medskip
\noindent{\em
%Combining classical logic, sequent calculus, abstract machines dependencies:
A core classical sequent calculus with dependent types}.
Dependent types are a key feature of type systems, typically
used in the context of both richly-typed programming languages and
proof assistants. Control operators, which are connected with classical
logic along the proof-as-program correspondence, are known to misbehave
in the presence of dependent types~\footcite{herbelin:tlca05}, unless
dependencies are restricted to values.
%As a step in his work to develop a sequent-calculus version of Hugo Herbelin's
%$dPA_\omega$ system~\footcite{herbelin:hal-00697240},
Étienne Miquey proposed
a sequent calculus for classical logic and dependent types, as an extension of Curien-Herbelin's $\mu\tilde\mu$-calculus
with a syntactical restriction to the fragment of
negative-elimination free proofs of dependent types~\cite{miquey:hal-01375977}.
%% The corresponding type system includes a list of explicit dependencies,
%% which maintains type safety. He showed that a continuation-passing style
%% translation can be derived by adding delimited continuations, and
%% how a chain of dependencies can be related to a manipulation of the return type
%% of these continuations.
%This work has been presented at ESOP 2017~\cite{miquey:hal-01375977}.
%\medskip
%\noindent{\em A classical sequent calculus with dependent types for
% arithmetic}.
The previous calculus has been extended to arithmetic in finite types
with strong elimination of existential quantification, thus
providing a sequent calculus
%presentation
%of a classical arithmetic
%from Hugo Herbelin
which is strong enough to prove the axiom of
dependent choice~\cite{miquey:tel-01653733}.
%% Getting classical logic and choice
%% together without being inconsistent is made possible by: (1)
%% constraining strong elimination of existential quantification to
%% proofs that are essentially intuitionistic; (2) turning
%% countable universal quantification into an infinite conjunction of
%% classical proofs, which are evaluated along a call-by-need evaluation strategy, so
%% as to extract from them intuitionistic contents that complies to the
%% intuitionistic constraint put on strong elimination of existential
%% quantification.
%% Relying on its sequent calculus with dependent types and its realisability
%% interpretation for call-by-need with control, Étienne Miquey proposed in his
%% thesis a sequent calculus with the same computational features~\cite{miquey:tel-01653733}.
%% His calculus therefore also allows for the direct definition of proof terms
%% for the axioms of countable and dependent choices.
The proofs of normalisation and soundness are made through a
realisability interpretation of the calculus, which is obtained by
using Danvy's methodology of semantic artifacts (work
%. This paper was
presented at LICS 2018, cf. Section 1).
%2018, where it received the Kleene award of the best student paper.
\medskip
\noindent{\em Call-by-need}.
%\noindent{\em Applying realisability to a combination of call-by-need,
% classical logic and sequent calculus: Normalisation and
% realisability interpretation of call-by-need with control}.
The call-by-need evaluation strategy is an evaluation strategy of the
$\lambda$-calculus which evaluates arguments of functions only when
needed, and then shares their evaluations across all places
where the argument is needed. %% The call-by-need evaluation is for
%% instance at the heart of a functional programming language such as
%% Haskell. A continuation-passing-style semantics for call-by-need, de
%% facto giving a semantics to control operators, was proposed in the 90s
%% by Okasaki, Lee and Tarditi. However, this semantics does not ensure
%% normalisation of simply-typed call-by-need evaluation, thus failing to
%% ensure a property which holds in the simply-typed call-by-name and
%% call-by-value cases.
Étienne Miquey and Hugo Herbelin have proved the normalisation of
Ariola et al.'s call-by-need $\lambda$-calculus by means of a variant of realisability whose realisers are pairs of a term and a
substitution (work presented at
FOSSACS 2018). %% This paves the way to give interpretation of calculus
%% with global and mutable memory.
%\medskip
%\noindent{\em Analysis of reduction in an abstract machine for classical call-by-need }.
Alexis Saurin, in collaboration with Pierre-Marie Pédrot, extended their previous work on the reconstruction of call-by-need based on linear head reduction with control. They showed how linear head reduction could be adapted to the $\lambda\mu$-calculus. %% This classical linear head reduction lifts the usual properties of the intuitionistic one (with respect to $\sigma$-equivalence) to the $\lambda\mu$-calculus (and its $\sigma$-equivalence already formulated by Olivier Laurent in his PhD thesis).
They showed for instance that substitution sequences of the $\lambda\mu$-calculus' linear head reduction are in correspondence with the classical Krivine abstract machine substitution sequences, validating the known fact that the KAM implements linear head reduction~\cite{pedrot:hal-01257348}. On top of this calculus, Kostia Chardonnet investigated levels of laziness as well as probabilistic call-by-need evaluation.
\medskip
\noindent{\it Call-by-name forcing for Dependent Type Theory}
Based on
Pierre-Marie Pédrot's investigation of variants of the forcing construction via decomposition through call-by-push-value~\cite{pedrot:tel-01247085}, Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau studied a variant of the forcing translation for dependent type theory, moving from the call-by-value variant to a call-by-name version which naturally preserves definitional equalities, avoiding the coherence pitfalls of the former one. It allows to show various metatheoretical results in a succinct fashion, notably for the independence of axioms~\cite{jaber:hal-01319066}. %% Work is ongoing to produce more positive results including abstracting reasoning on step-indexing using this technique.
%This work was presented at LICS 2016.
\medskip
\noindent{\em Gödel's functional interpretation}.
Pierre-Marie Pédrot gave a computational analysis of Gödel's
``Dialectica'' interpretation in terms of collecting stacks
in an abstract machine~\cite{pedrot:tel-01247085}. His work also
includes Dialectica for type theory, with dependent elimination.
\medskip
\noindent{\em Forcing and classical realisability}.
In collaboration with Boban Velickovic, Alexis Saurin advised the LMFI
master internship of Ikram Cherigui on classical realisability and
forcing in set theory.
\medskip
\noindent{\em The computational contents of completeness proofs}.
Hugo Herbelin developed an original and simple proof of Gödel's
completeness theorem with side-effects which he presented in
workshops.
%\paragraph{Alternative syntaxes for proofs}
%
%Amina Doumane and Alexis Saurin, in a joint work with Marc Bagnol, studied the structure of correctness criteria for linear logic proof-nets and could connect and compar several known criteria via a primitive notion of dependency. This work was first presented at JFLA 2014~\cite{bagnol:hal-01110338} early 2014 and later at Structure and Deduction in Vienna as part of FLOC 2014. An expanded version has recently been accepted at FOSSACS 2015~\cite{bagnol:hal-01110340}.
%% \paragraph{Effectful proving}
%% Hugo Herbelin started a program of reconstruction of different levels
%% of computational strength of logic by means of translation to a core
%% logic of polarised linear connectives.
%% With the goal of transferring the effectful computational contents of
%% the dependent choice to other forms of choice or bar induction axioms,
%% Hugo Herbelin worked at clarifying the folklore regarding the
%% strengths of various forms of choice and of bar induction.
\paragraph{Reverse mathematics}
Reverse mathematics were studied from a provability point of view and
a computational point of view, in
the context of the subsystems of classical second-order arithmetic and of
intuitionistic reverse mathematics of different forms of the axiom of
choice, respectively.
\medskip
\noindent{\em Ramsey-type reverse mathematics}.
Ludovic Patey studied with Laurent Bienvenu and Paul Shafer the
provability strength of Ramsey-type versions of theorems like König's
lemma~\cite{bienvenu:hal-01888542}. Ludovic Patey studied with Laurent Bienvenu the
constructions of diagonal non-computable functions by probabilistic
means (paper submitted). Ludovic
Patey worked on the existence of universal instances in reverse
mathematics~\cite{patey:hal-01888599}. He worked on the relations between diagonal non-computability
and Ramsey-type theorems~\cite{patey:hal-01888596}. He studied the links between the iterative
forcing framework developed by Lerman, Solomon and Towsner and the
notion of preservation of hyperimmunity~\cite{patey:hal-01888601}.
\medskip
\noindent{\em Reverse mathematics of Gödel's completeness theorem}.
Charlotte Barot, under the supervision of Hugo Herbelin, studied the
relative intuitionistic strength of Gödel's completeness theorem,
the ultrafilter lemma, and different forms of the Fan Theorem, as a
way to transfer computational contents of proofs from one to the other
theorems.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Collaborations}
% {\footnotesize\sl List the partners with whom you had a strong and fruitful collaboration during the evaluation period (joint publications, joint software development) and refer to the topic and the outcome of the collaboration. TBR}
The team had a collaboration with ANSSI (Agence Nationale pour la
Sécurité des Systèmes Informatiques), with Univ. of Cambridge
(Fiore), Univ. of Tallinn, indirectly the
Haskell development team and Univ. of Göteborg via our
collaboration with Tweag I/O, Univ. de la República (Uruguay)
(Miquel), Univ. of Rosario, with the Logic
team (Velickovic) of the joint Math lab between Univ. Paris 7 and Univ. Paris 6,
Univ. of Montpellier (Bienvenu), with Univ. of
Gent (Shafer). We had the following visitors:
Marcelo Fiore (Univ. of Cambridge, two weeks
in February 2017),
Mauro Jaskelioff (National Univ. of Rosario and CONICET,
Argentina, one week in May 2018),
Tarmo Uustalu (Univ. of Tallinn and Univ. of Reykjavik, two weeks in 2017 and two weeks in
2018).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{External support}
% {\footnotesize\sl List the various support you had, e.g. Inria project labs, national initiatives (ANR, PIA, etc), European and international projects, industrial contracts. This subsubsection must be very short. Details should be provided in section \ref{finance}. TBR.}
The team benefited from an invitation program to collaborate with
Marcelo Fiore; from the PHC Parrot with Estonia to
collaborate with Tarmo Uustalu; from the joint lab LIA
IFUM with Uruguay; from the ANR Récré (réécriture et
réalisabilité). There are contacts with ANSSI for giving a formal status
to our cooperation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Self assessment}
% {\footnotesize\sl Outline the strong and the weak points. What should be continued, modified, stopped? TBR.}
The theoretical research done in the team in either proof theory,
program semantics, or at the junction between logic and computer
science, especially regarding side effects, is original and
foundational. The work on programming with side effects in Coq is also
crucial to go in the direction of Coq as general-purpose programming
language for certified sofware.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Research axis 2: Reasoning and programming with infinite data} \label{Research-axis-2}
%{\footnotesize\sl There should be one such subsection for each main research axis of the project-team during the evaluation period. Each subsection should be approximatively 3 pages long. The number of main research axes (and therefore of such subsections) is expected to be less than 5, typically 3. For each subsection, fill the following subsubsections when appropriate. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Personnel}
%{\footnotesize\sl List the team members involved in this line of research (1-2 lines). TBR.}
Permanent members: Yann Régis-Gianas, Alexis Saurin. Postdocs: Guilhem Jaber, Luc Pellissier, Andrew Polonsky. PhD students: Amina Doumane, Pierre-Marie Pédrot, Abhishek De. Interns: Paul Laforgue, Rémi Nollet, Xavier Onfroy, Sylvain Ribstein.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Project-team positioning}
%{\footnotesize\sl Should be about half a page. Positioning of the project wrt the state of the art and with regards to other INRIA project-teams and other national/international research groups (peer or competitor groups). TBR.}
Our positioning on this topic arose as a cross fertilisation of proof theory and programming language theory
%by the development of Curry-Howard correspondence
in the field of logics expressing least and greatest fixed points properties and of temporal logics. Such logics allow to express (co)inductive reasoning, and the computational content is related with (co)inductive types and (co)recursive programming.
%
Proof systems for fixed point logics can naturally be obtained by taking
(co)induction rules that closely reflect fixed point theorems,
e.g.\ Knaster-Tarski's characterisation of least fixed points as least
pre-fixed points.
This is the case of Kozen's famous axiomatisation~\footcite{kozen83tcs}.
When building proofs using such rules, (co)invariants have to be found, possibly significantly more complex than the property to establish. An alternative to these
explicit (co)induction rules is to consider proof systems featuring
non-wellfounded derivation trees: this makes it possible to reason on
fixed points by unfolding them, possibly infinitely often. However, the soundness of such systems requires a global
\emph{validity} condition.
%
An important question is the comparison of such proof systems with usual systems with induction and coinduction rules à la Park. Recent results on Brotherston-Simpson's Conjecture showed that circular provability is equivalent to finitary one in presence of arithmetics for the theory of Martin-Löf's inductive definitions. However, no such general result is known for the $\mu$-calculus.
The aim of the team is to develop the (non-wellfounded) proof theory of such logics and to study their computational content via semantical studies as well as Curry-Howard correspondence.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Scientific achievements}
%{\footnotesize\sl Describe the main contributions in 1 page. Emphasize their originality, significance and impact. Refer to the main results: publications, theses, software. TBR.}
This theme is part of the ANR project RAPIDO (see the National
Initiatives section).
\paragraph{Proof Theory of Non-Well-Founded Proofs}
The team contributed to the definition of new infinitary proof systems for fixed point logics where proofs can have non-wellfounded branches. Known systems were extended in three directions: new logical languages (multiplicative additive linear logic, $\mu$MALL), more flexible validity conditions (by allowing threads to bounce on axiom and cut rules) and new formal proof systems.
Contributions to their meta-theory were made.
\medskip
\noindent{\it From straight to bouncing threads.}
After their initial work on $\mu$MALL infinitary and circular proofs establishing cut-elimination and focalisation~\cite{baelde:hal-01339037}, in collaboration with David
Baelde and Denis Kuperberg (from ENS Cachan and Lyon), Amina Doumane, Guilhem Jaber and Alexis Saurin extended non-wellfounded proofs, by relaxing the validity condition allowing threads to move not only up in the proofs but also down by bouncing on axiom and cut inferences. Cut-elimination is proved and decidability of the criterion is investigated in the multiplicative case (work submitted)
%
An effort in formalising in Coq circular proofs and the decidability of their validity (with straight threads) was started by Alexis Saurin together with Xavier Onfroy during the summer 2018 while Alexis Saurin and Rémi Nollet (from IRIF) started investigating the complexity of deciding validity by relating their validity to size-change termination.
% to address its PSPACE-completeness.
\medskip
\noindent{\it Other studies on circular proof formalisms.}
Amina Doumane and Alexis Saurin, in a joint work with David Baelde~\cite{baelde:hal-01256773},
developed
a game-semantics of $\mu MALL$.
%More recently, Alexis Saurin and Guilhem Jaber developed a circular natural deduction for a circular $\lambda$-calculus with inductive and coinductive types.
The definition of the bouncing validity condition helped in better understanding the relations and discrepancy between the parallel nature of threads and the sequential nature of proofs, which motivated the PhD topic of Abhishek De (advised by Alexis Saurin).
\medskip
\noindent{\it Finitising Circular Proofs.}
%
Amina Doumane proposed in her PhD a translatability criterion for finitising circular proofs. In a work with Rémi Nollet and Christine Tasson from IRIF, Alexis Saurin presented a new validity condition which can be checked at the level of elementary cycles, while the other criteria need to check a condition on every infinite branch. They still capture all circular proofs from $\mu MALL$ finite proofs~\cite{nollet:hal-01825477} and obtained partial finitisation results.
\medskip
\noindent{\it Automata Theory Meets Proof Theory.}
In a joint work with David Baelde and Lucca Hirschi (from ENS Cachan),
Amina Doumane and Alexis Saurin carried out a proof-theoretical
investigation of the linear-time $\mu$-calculus (LT$\mu$),
proposing well-structured proof systems and showing constructively
their completeness for formulas expressing inclusions of Büchi automata~\cite{doumane:hal-01275289}.
Amina Doumane then extended the result and obtained a constructive proof of completeness for full LT$\mu$.
In order to achieve this tour de force,
she identified fragments of LT$\mu$ corresponding to various classes of $\omega$-automata and proved their completeness by using circular proof systems and finitisation of the infinite proofs in Kozen's usual axiomatisation~\cite{doumane:hal-01430737} (cf. Section 1) .
%She received the Kleene award
%of the best student paper and the ``Prix scientifique de {\it La Recherche}'' for the best French 2017 computer science paper.
\paragraph{Programming with fixed points, infinite data and time} In this part, we collect work on the $\lambda (Y)$-calculus, copatterns, and preliminary work on Functional Reactive Programming (FRP).
\medskip
\noindent{\it Fixpoint conjectures.}
With Giulio Manzonetto (from LIPN, Université Paris Nord), Andrew Polonsky (from Appalachian State Univ.) and Jakob Simonsen (from DIKU, Denmark), Alexis Saurin studied two long-standing conjectures on the $\lambda$-calculus: the ``fixpoint property'' and the ``double-fixpoint conjecture''\footnote{The former asserts that every $\lambda$-term admits either a unique or an infinite number of $\beta$-distinct fixpoints while the second, formulated by Statman, says that there is no fixpoint satisfying $Y\delta=Y$ for $\delta=\lambda y,x.x(yx)$.}. Their results are currently submitted to a journal~\cite{manzonetto:hal-01672846}.
%
Moreover, Andrew Polonsky and Alexis Saurin defined an infinitary $\lambda$-calculus allowing transfinite iteration of abstractions and ordinal sequences of applications, $\Lambda^o$, and established a standardisation theorem for this calculus in which the $\Lambda\mu$-calculus (as well as the Stream Hierarchy) can be embedded.
\medskip
\noindent{\it Co-Patterns.}
With Paul Laforgue, Yann Régis-Gianas
studied the mechanisms of co-patterns
%introduced by Abel and Pientka
from a programming language
perspective, defining an untyped version as well as an abstract
machine.
% to efficiently evaluate cofunctions.
%
They designed an extension of OCaml with copatterns,
%. They
showed that
copattern-matching can be added with no effort to any programming
language equipped with second-order polymorphism and generalised
algebraic datatypes (work presented at PPDP 2017 and
JFLA 2018~\cite{laforgue:hal-01897456}).
\medskip
\noindent{\it Functional Reactive Programming.}
With Sylvain Ribstein, Yann Régis-Gianas defined an OCaml library for
differential FRP (DFRP) extending FRP with the
ability to modify past events and compute the consequences of
this modification in all the events that depend on it.
%
Rémi Nollet studied (during his master supervised by Alexis Saurin and Christine Tasson) the recent extension of
Curry-Howard correspondence between FRP and linear temporal logic
(LTL) as well as various natural deduction and sequent systems for LTL and compared them to type systems for FRP.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Collaborations}
%{\footnotesize\sl List the partners with whom you had a strong and fruitful collaboration during the evaluation period (joint publications, joint software development) and refer to the topic and the outcome of the collaboration. TBR}
Strong collaborations on this topics were developed with LSV (ENS Cachan) and LIP (ENS Lyon) thanks to the RAPIDO Project, as well as with LIPN (Univ. Paris 13), as well as with a number of international collaborators with the set up of the PARIS workshop on the theme of this research axis, organised during FLOC 2018 in Oxford, of which followups are being organised.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{External support}
%{\footnotesize\sl List the various support you had, e.g. Inria project labs, national initiatives (ANR, PIA, etc), European and international projects, industrial contracts. This subsubsection must be very short. Details should be provided in section \ref{finance}. TBR.}
The ANR Project RAPIDO started in January 2015 and will end in late September 2019. The project funded post-docs (Guilhem Jaber, Luc Pellissier and Andrew Polonsky) and visits, as well as the organisation of the above-mentioned PARIS workshop.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Self assessment}
%{\footnotesize\sl Outline the strong and the weak points. What should be continued, modified, stopped? TBR.}
This theme is rather new in the team.
Connections with the practice and development of proof assistants are not yet achieved but the proof theory of logics with induction and coinduction as well as the dynamics of those proofs have been significantly developed during the evaluation period.
This opens several directions for future investigations in areas where the concept of Curry-Howard correspondence is emerging and not fully understood (for instance in the setting of FRP).
One weakness is that this axis was boosted by the support of the ANR project which is coming to an end. Still, a network of collaborators has been built which could lead either to broader projects (networks and ERC Synergy grant), or/and to smaller-scale, lighter projects such a associated teams (for instance with researchers from Gothenburg Univ., Sweden).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Research axis 3: Effective higher-dimensional algebra} \label{Research-axis-3}
% {\footnotesize\sl There should be one such subsection for each main research axis of the project-team during the evaluation period. Each subsection should be approximatively 3 pages long. The number of main research axes (and therefore of such subsections) is expected to be less than 5, typically 3. For each subsection, fill the following subsubsections when appropriate. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Personnel}
% {\footnotesize\sl List the team members involved in this line of research (1-2 lines). TBR.}
Permanent members: Pierre-Louis Curien, Yves Guiraud, Matthieu Sozeau. Postdoc: Eric Finster. PhD students: Antoine Allioux, Cyrille Chenavier, Cédric Ho Thanh, Maxime Lucas, Jovana Obradović. Interns: Amina Bendjaafar, Joey Beauvais-Feisthauer, Jean Vassalo. External collaborators: Philippe Malbos (Univ.\ Lyon~1), Samuel Mimram (École Polytechnique).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Project-team positioning}
% {\footnotesize\sl Should be about half a page. Positioning of the project wrt the state of the art and with regards to other INRIA project-teams and other national/international research groups (peer or competitor groups). TBR.}
The team was involved in the ANR Cathre project (2014-2017), coordinated by Pierre-Louis Curien, comprising most of the French researchers active in the field of the algebraic and homotopical aspects of higher categories. We actively participate to the PPS working group on higher categories, a nationally recognised seminar. In the last years, we have continued to organise international events to promote effective methods in higher algebra, to create connections with other related research directions, and to increase our international visibility: the Higher-Dimensional Rewriting and Algebra workshop in 2015, 2016, 2017 and 2018, and the Categories in Homotopy and Rewriting conference at the CIRM in Marseille in 2018.
Three current INRIA teams have close research activities. Ouragan and Polsys, at INRIA Paris, also investigate the use of rewriting-like methods, mainly based on Gröbner bases, with applications to the resolution of polynomial systems. Gallinette, at INRIA Nantes, also explores the higher structures that occur in homotopy type theory, and the formalisation of polygraphs in Coq.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Scientific achievements}
% {\footnotesize\sl Describe the main contributions in 1 page. Emphasize their originality, significance and impact. Refer to the main results: publications, theses, software. TBR.}
\paragraph{Rewriting methods in higher algebra}
With Stéphane Gaussent (Univ.\ Saint-Étienne) and Philippe Malbos (Univ.\ Lyon~1), Yves Guiraud applied rewriting methods to Artin monoids~\cite{gaussent:hal-00682233}, improving results in representation theory: one by Tits about the presentation complex of Artin monoids~\footcite{Tits81}, and one by Deligne about the actions of Artin monoids on categories~\footcite{Deligne97}. This work introduces a homotopical extension of the Knuth-Bendix completion procedure (see also~\footcite{GuiraudMalbosMimram13}), that was partly implemented as the Cox library and in the Rewr prototype.
With Eric Hoffbeck (Univ.\ Paris~13) and Philippe Malbos, Yves Guiraud has developed a theory of rewriting for associative algebras~\cite{guiraud:hal-01006220}, with a view towards applications in homological algebra, generalising both Gröbner bases~\footcite{Buchberger} and Poincaré-Birkhoff-Witt bases~\footcite{Priddy}. They transposed the construction of~\footcite{GuiraudMalbos12} to compute small polygraphic resolutions of associative algebras with rewriting methods. This construction gave necessary or sufficient conditions for an algebra to have the homological property of Koszulness.
With Philippe Malbos, Yves Guiraud has written a survey (targeted for graduate students) on the use of rewriting methods in algebra, in the language of higher categories~\cite{guiraud:hal-00932845}
%, intended as an introduction to the domain, mainly for graduate students.
Moreover, Yves Guiraud has written his ``Habilitation à diriger des recherches'' manuscript, on rewriting methods in higher algebra~\footcite{Guiraud19} (defence planned is Spring 2019).
Cyrille Chenavier (PhD supervised by Yves Guiraud and Philippe Malbos~\cite{chenavier:tel-01415910}), has explored Berger's theory of reduction operators~\footcite{Berger98} to improve noncommutative Gröbner bases. He used a lattice structure to give a new algebraic characterisation of confluence, a new completion algorithm~\cite{chenavier:hal-01325907}, connected to Faugère's F4 procedure~\footcite{FaugereF4}, and a method to compute a linear basis of the space of syzygies of a set of reduction operations~\cite{chenavier:hal-01578555}. Moreover, in this setting, normalisation strategies are related through braid-like relations, leading to new constructions in homological algebra~\cite{chenavier:hal-01141738}.
Maxime Lucas (PhD supervised by Yves Guiraud~\cite{lucas:tel-01668359}) has improved the rewriting techniques of~\footcite{GuiraudMalbos12mscs} to obtain coherence theorems for bicategories, pseudofunctors and pseudonatural transformations~\cite{lucas:hal-01191867}. He transposed to a cubical setting, and improved, the results of~\footcite{GuiraudMalbos12}. This involved a theoretical work on the connections between globular and cubical higher categories~\cite{lucas:hal-01662127}, generalising several already known links in a unique setting~\footcite{BrownHiggins1, BrownHiggins2, AlAglBrownSteiner, Steiner}. He proved a cubical version of Squier's theorem~\cite{lucas:hal-01662132}.
With Patrick Dehornoy (Univ. Caen), Yves Guiraud has developed an axiomatic setting for monoids with a local normalisation procedure~\cite{dehornoy:hal-01141226}, generalising both normalisation by a quadratic rewriting system and Garside normalisation~\footcite{DehornoyDigneGodelleKrammerMichel13}. This induced a new sufficient condition for a rewriting system to terminate, based on the length of normalisation paths on length-three words. This opened the way to improvements of rewriting methods coming from Garside theory, leading both to new methods in higher algebra, and to a new enhanced completion procedure in rewriting theory (ongoing collaboration between Yves Guiraud and Matthieu Picantin from IRIF).
\paragraph{Metatheoretical work on and categorification of cyclic operads}
Pierre-Louis Curien and Jovana Obradović developed in \cite{curien:hal-01278214} a syntactic approach (using some of the kit of Curien-Herbelin's duality of computation and its polarised versions by Munch and Curien) to the definition of various structures that have appeared in algebra under the names of operads, cyclic operads, dioperads, properads, modular and wheeled operads, permutads, etc. Their goal was to formalise the proofs of equivalence between various styles of definition in the literature. This was done for cyclic operads by Jovana Obradović \cite{obradovic:tel-01676983}.
Pierre-Louis Curien and Jovana Obradović
pursued their work on cyclic operads by establishing the notion of categorified cyclic operad, where the axioms are weakened from equalities to natural isomorphisms, and by formulating conditions concerning these isomorphisms which ensure coherence~\cite{curien:hal-01679682}.
%This coherence is of the same kind as the coherence of symmetric monoidal categories: all diagrams made of associator and commutator isomorphisms are required to commute. However, in the setting of cyclic operads, where the existence of objects and morphisms depends on the shape of a fixed unrooted tree, these arrows do not always exist.
%Pierre-Louis Curien and Jovana Obradović exhibited the appropriate conditions (different from those of Mac Lane) and
%They proved a coherence theorem}, relying on a result of Do\v sen and Petrić on the coherence of categorified operads.
As a companion to these works,
in collaboration with Jelena Ivanović, Pierre-Louis Curien and Jovana Obradović have introduced an inductively defined tree notation for all the faces of polytopes arising from a simplex by truncations, and have provided many examples of its use.
%, that allows them to view inclusion of faces as the process of contracting tree edges.
%This notation instantiates to the well-known notations for the faces of associahedra and permutohedra.
%They built on Do\v sen and Petrić's hypergraph polytopes, which describe the interval of polytopes from the simplex to the permutohedron.
%This interval was further stretched by Petrić to allow truncations of faces that are themselves obtained by truncations, and iteratively so. The notation developed by the three authors applies to all these polytopes.
In their work, they also explored links between polytopes and categorified operads
%, as a follow-up of another work of
% Do\v sen and Petrić, who had exhibited some families of hypergraph polytopes (associahedra, permutohedra, and
%hemiassociahedra) describing
% the coherences, and the coherences between coherences etc., arising in higher operads:
%a criterion allowing to recover the information whether edges of these ``operadic polytopes'' come from sequential, or from parallel associativity is established
~\cite{obradovic:hal-01669490}.
\paragraph{Opetopes}
Opetopes are a formalisation of higher many-to-one operations, leading to one of the approaches for defining weak $\omega$-categories. Opetopes were originally defined by Baez and Dolan. A reformulation (leading to a more carefully crafted definition) has been later provided by Batanin, Joyal, Kock and Mascari, based on the notion of polynomial functor. Pierre-Louis Curien, Cédric Ho Thanh and Samuel Mimram have developed (in several variants) a type-theoretical treatment of opetopes and finite opetopic sets, and have shown that the models of their type theory are indeed the opetopic sets as defined by the above authors (work submitted).
\paragraph{Type theory and higher algebra}
Eric Finster explored the connections between intensional type theory and the theory of higher topoi, as developed in the works of Joyal and Lurie~\footcite{LurieHT}. In particular, in collaboration with Mathieu Anel, André Joyal and Georg Biedermann, he gave a proof of a new result about the generation of left exact modalities in higher topoi, which has a corresponding internalisation in homotopy type theory. Applications of this result to the Goodwillie calculus (an advanced technique in abstract homotopy theory) resulted in the article~\cite{anel:hal-01939906}.
Antoine Allioux (PhD started in February 2018), Eric Finster, Yves
Guiraud and Matthieu Sozeau are exploring the development of higher
algebra in type theory based Eric Finster's internalisation of
polynomial monads (of which opetopes and $\infty$-categories are
instances) in type theory. This should provide a way to build %a host of
coherent higher structures in type
theory. Antoine Allioux is focusing on showing the equivalence between
categories seen as polynomial monads and the standard univalent
categories of homotopy type theory~\footcite{hottbook}. Polynomial
monads also provide a solution to the long-standing open problem of defining
simplicial types in homotopy type theory.
%An article on this subject is in preparation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Collaborations}
% {\footnotesize\sl List the partners with whom you had a strong and fruitful collaboration during the evaluation period (joint publications, joint software development) and refer to the topic and the outcome of the collaboration. TBR}
Yves Guiraud collaborated with Patrick Dehornoy (Univ.\ Caen), Stéphane Gaussent (Univ.\ Saint-Étienne), Eric Hoffbeck (Univ.\ Paris~13), Philippe Malbos (Univ.\ Lyon~1) and Samuel Mimram (École Polytechnique), leading to four publications in international journals and to the development of the Rewr prototype. He currently works with Marcelo Fiore (Univ.\ Cambridge) on the first article of a planned series, and with Matthieu Picantin (Univ.\ Paris~7) on two articles. Pierre-Louis Curien collaborates with Bérénice Delcroix-Oger (from IRIF) on a follow-up of his work on hypergraph polytopes. Their goal is to investigate and unify various algebraic structures (known and new) on the faces of some families of polytopes.
We had the following
visitors: John Baez (Univ.\ California Riverside, one week in Nov.~2017), Marcelo Fiore (Univ.\ Cambridge, two weeks in Feb.~2017), Jovana Obradović (Univ.\ Prague, ten days in Dec.~2018).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{External support}
% {\footnotesize\sl List the various support you had, e.g. Inria project labs, national initiatives (ANR, PIA, etc), European and international projects, industrial contracts. This subsubsection must be very short. Details should be provided in section \ref{finance}. TBR.}
This axis has benefited from the support of the IDEX Sorbonne-Paris-Cité Focal project, 2013-2016 (including\ Cyrille Chenavier's PhD grant),
the ANR Cathre project, 2014-2017 (including\ Maxime Lucas' PhD grant), and the ERC CoqHoTT, INRIA Gallinette, Nantes (including\ Eric Finster's postdoc and Antoine Allioux's PhD grant).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Self assessment}
% {\footnotesize\sl Outline the strong and the weak points. What should be continued, modified, stopped? TBR.}
The team members have contributed to the development of effective methods in higher algebra, in France and abroad, leading to new results in representation theory and in homological algebra. These methods are now investigated in other places, following collaborations or dissemination of former students: Lyon, Saint-Étienne, Marseille, Nantes, Lille, Prague, etc.
New potential applications have been investigated, such as the development of rewriting methods on Lie algebras, but the current known techniques are too limited to apply directly and will have to be improved
(for example with the integration of Garside theory in our toolbox).
Over the last years, several unforeseen theoretical obstructions have slowed down the work we have conducted (such as the complexity of the higher structures involved in rewriting theory on noncommutative polynomials), leading to a lower-than-expected software development. %that we hope to resume at a faster pace in the coming years.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Research axis 4: Incrementality} \label{Research-axis-4}
% {\footnotesize\sl There should be one such subsection for each main research axis of the project-team during the evaluation period. Each subsection should be approximatively 3 pages long. The number of main research axes (and therefore of such subsections) is expected to be less than 5, typically 3. For each subsection, fill the following subsubsections when appropriate. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Personnel}
% {\footnotesize\sl List the team members involved in this line of research (1-2 lines). TBR.}
Permanent members: Yann Régis-Gianas. PhD Students: Thibaut Girka, Lourdes del Carmen González Huesca. Interns: Kostia Chardonnet, Colin Gonzalez.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Project-team positioning}
% {\footnotesize\sl Should be about half a page. Positioning of the project wrt the state of the art and with regards to other INRIA project-teams and other national/international research groups (peer or competitor groups). TBR.}
This research axis investigates a language-oriented approach to
incremental computations. A computation is incremental when it
consists of a sequence of small changes of its output in reaction to a
sequence of small changes of its (large) input. Typically, if $f : A
\rightarrow B$, then we are interested in computing the sequence $y_i =
f\,x_i$ where the difference between~$x_i$ and~$x_{i + 1}$ is small
comparing to the size of~$x_i$. Incremental computations are
especially relevant in software development, because software is built
by many patches; in machine learning, because statistical models are
refined through many observations of a large dataset; or in
blockchains, because the chain is built by small increments.
Our investigations in this research axis are primarily focused on the
following question: what is a good language to express provable and
efficient incremental computations? Around 2010, the state of the art
about language-based incremental computation was the PhD thesis of
Umut Acar about self-adjusting computations. In this work, Umut Acar
designed a very efficient computational model to automatically
incrementalise programs. Unfortunately, reasoning about the
algorithmic complexity of the resulting incremental programs requires
reasoning about complex dynamic mechanisms and objects (e.g.\ change
propagations and dependency graphs of memoised computations). As a
result, it is quite hard for a programmer to predict (and, by
extension, to prove properties about) the efficiency of programs
written in this style.
Since 2013, several teams (Klaus Ostermann in
Tübingen Univ., Tiark Rompf in Purdue Univ., Conal
Elliott from a data science company named \emph{Target}, Martin
Abadi from Google, etc) are trying to achieve the same kind of
efficient computational models but using more declarative
languages. In these differential programming languages,
incrementalisation is obtained by means static program
transformations so that reasoning about an incremental program is a
standard proof of program. Our work is focusing on
differential higher-order functional programs computing over
non-numerical domains while most of the aforementioned teams are
implementing efficient declarative programming models to automatically
differentiate first-order numerical programs. On the topic of
$\lambda$-terms' static differentiation, we collaborated with Klaus
Ostermann's team.
One interesting application of differential programming is the
specification and certification of software evolutions, as initiated
by Thibaut Girka, whose PhD thesis was funded by Mitsubishi
Electrics. By constructing a (non-numeric) domain for program semantic
differences, we provide a foundational framework to perform relational
reasoning about the difference of behaviour between programs. The
verification of software evolutions is an important topic in the
verification community, with strong contributions by teams from
Microsoft Research, IMDEA, Univ. of Technion, and IRIF. Comparing
to these approaches which prioritise automation, we focus on
expressivity: for instance, we are able to reason about bugfixes
while other approaches of the literature cannot.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Scientific achievements}
% {\footnotesize\sl Describe the main contributions in 1 page. Emphasize
% their originality, significance and impact. Refer to the main
% results: publications, theses, software. TBR.}
\paragraph{Differential programming language}
Lourdes González and Yann Régis-Gianas developed
a new variant of the differential $\lambda$-calculus that has two main
features: (i) it is deterministic; (ii) it is based on a notion of
first-class changes. An extension of the simply-typed $\lambda$-calculus
with differentials and partial derivatives offers a language to reason
about incrementality. The basic system, $\lambda$-diff, was enriched
with expressions for fixpoints and data-types together with their
corresponding derivatives to analyse incrementality over them. The
above results are reported in the second part of Lourdes González'
PhD thesis~\cite{gonzalezhuesca:tel-01248531}.
In collaboration with Paolo Giarrusso, Philipp Schuster and Yufei Cai
(Univ.\ Marburg, Allemagne), Yann Régis-Gianas developed a new method to
statically incrementalise higher-order programs using formal
derivatives and static caching. This method overcomes a defect
of previous approaches to static differentiation of
programs by sharing information between base computations and
incrementalised computations. He developed a
mechanised proof for this transformation, as well as a prototype
language featuring efficient derivatives
for functional programs.
Differential functional programming is new, and some exploratory work
is needed to understand what are its idioms. In collaboration with
Olivier Martinot (Univ.\ Paris~7), Yann Régis-Gianas studied a new
technique to implement incrementalised operations on lists. In
collaboration with Colin Gonzalez, Yann Régis-Gianas developed BLACS,
a programming framework that applies differential functional
programming techniques to the implementation of asynchronous
spreadsheets for big data. In collaboration with Lelio Brun (ENS),
Yann Régis-Gianas developed DeltaCoq, a library for certified
incremental functional programming.
\paragraph{Difference languages}
In collaboration with David Mentré (Mitsubishi), Thibaut Girka and
Yann Régis-Gianas designed a new algorithm for
correlating program generation: such a program is used to characterise
the differences between two close programs.
% (Therefore, a correlating
%program is a good input for an incremental static analyser.)
Before
their work, only one, unsound. algorithm existed in the literature. The new algorithm is sound and certified in Coq~\cite{girka:hal-01238704}.
%This work
%has been presented at the ATVA conference. Thibaut Girka has presented
%this work at ATVA 2015.
They also designed a metatheoretical framework to develop
verifiable difference languages in Coq. Such formal differences
capture semantic differences between close programs and overcome
existing systems in terms of expressivity~\cite{girka:hal-01653283}.
%Thibaut Girka and Yann
%Régis-Gianas presented this work in several working groups: Gallium
%(Paris), ``Journée annuelle du groupe LTP'' of the GDR GPL (Saclay),
%LIMA (Nantes), IRIF (Paris).
Kostia Chardonnet and Yann Régis-Gianas started the formalisation of
difference languages for Java, using the framework developed by
Thibaut Girka. In particular, Kostia Chardonnet implemented a
mechanised small-step operational semantics for a large subset of
Java.
\subsubsection{Collaborations}
Yann Régis-Gianas collaborates with David Mentré (Mitsubishi Electrics, Rennes), with Paolo Giarrusso (EPFL, Suisse), with Philip
Schuster and Yufei Cai (Univ Marburg, Allemagne). We received the following visitors:
Paolo Giarrusso (Univ. of Marburg, February 2016),
Lourdes González (Univ. of Mexico, December 2016).
\subsubsection{External support}
The PhD thesis of Thibaut Girka was supported by Mitsubishi (CIFRE grant).
The PhD thesis of Lourdes González was funded
by the ANR project Paral-ITP.
\subsubsection{Self assessment}
% {\footnotesize\sl Outline the strong and the weak points. What should be continued, modified, stopped? TBR.}
The work done on differential $\lambda$-calculus is foundational: it
provides an important robust basis to build further research about
incremental computations. It is however a pity that the results of
Lourdes González' PhD thesis about differential $\lambda$-calculus
have not been published quickly enough: almost the same results have
been published at the same period by the team of Klaus
Ostermann. Fortunately, the competition with that team finally led
to a collaboration. Incremental programming is notoriously difficult:
our ability to certify incremental programs using Coq is a strength
that will be emphasised in the next years.
The theoretical framework of the PhD thesis of Thibaut
Girka has now to be scaled up to realistic programming languages that
interest the software engineering community.
% typically Java.
The
collaboration with Mitsubishi is continuing in that direction. A new
PhD thesis is planned to that end.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Research axis 5: Metatheory and development of Coq} \label{Research-axis-5}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\label{axis:Coq}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Personnel}
Permanent members: Hugo Herbelin, Pierre Letouzey, Yann Régis-Gianas,
Matthieu Sozeau. PhD students: Gaëtan Gilbert (Inria Nantes), Gabriel
Lewertowski, Cyprien Mangin, Théo Winterhalter (Inria Nantes), Théo
Zimmermann. Engineer: Thierry Martinez. Interns: Meven Bertrand, Philipp
Haselwarter, Vadim Zaliva. External Collaborators: Nicolas Tabareau
(Inria Nantes), Beta Ziliani (Córdoba, Argentina).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Project-team positioning}
% {\footnotesize\sl Should be about half a page. Positioning of the project wrt the state of the art and with regards to other INRIA project-teams and other national/international research groups (peer or competitor groups). TBR.}
This line of research centers around the study of dependent type
theories and their implementation, notably in the Coq proof assistant.
Within Inria, the Gallinette team, with which
we have a strong collaboration, and the Deducteam team are the closest. Internationally, dependent type theory is a very
active area of research, especially since the advent of homotopy type
theory, with many groups strongly focusing on it: Gothenburg (Thierry
Coquand), Nijmegen (Herman Geuvers), Nottingham (Thorsten Altenkirch),
Strathclyde (Neil Ghani), Aarhus (Lars Birkedal), Birmingham (Martin
Escardó), CMU (Steve Awodey, Robert Harper), Microsoft (Leo de Moura).
While many of these research groups concentrate on the semantical side, our
focus is more on the implementation side of proof assistants, for
applications to both programming and mathematics.
The \project team is at the forefront of the development of Coq. On the
theoretical side, the team has developed new extensions of the proof
assistant that put it at the state of the art in the treatment of
universes and cumulativity in type theory-based proof assistants (Agda,
Lean, RedPRL), along with formalising the unification algorithm of the
system whose interaction with universes is non-trivial. A recent
development coming after many years of maturation is the integration of
definitional proof-irrelevance in the system, which was developed in
collaboration with the Gallinette team and a member of the Agda
development team. The system is also gaining traction for the
development of dependently-typed programs through the \Equations
plugin which provides state-of-the-art compilation of dependent
pattern-matching and tools to reason on functional programs.
Development of Coq itself has become more decentralised and is a
collaborative effort managed mainly by the \project, Gallinette, Tocatta
and Marelle teams, with Matthieu Sozeau serving as project coordinator,
after Hugo Herbelin. More information about this can be found in Section 3.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Scientific achievements}
% {\footnotesize\sl Describe the main contributions in 1 page. Emphasize their originality, significance and impact. Refer to the main results: publications, theses, software. TBR.}
\paragraph{Cumulativity for Inductive Types}
Together with Amin Timany, Matthieu Sozeau developed the Calculus of
Cumulative Inductive Constructions, which extends the cumulativity
relation of universes to universe polymorphic inductive types~\cite{timany:hal-01952037}.
%This work was presented at FSCD 2018}.
Its consistency
model~\cite{timany:hal-01615123} suggested a suprising relaxation of the
subtyping relation on inductive types in Coq, able to model the
previously ad-hoc treatment of polymorphism for inductive types. This
work provides a state-of-the-art universe system for Coq, with
applications to formalisations of homotopy type theory like is done in
the HoTT library~\cite{bauer:hal-01421212},
category theory and syntactic translations of type theory
\footcite{boulier:hal-01445835}.
\paragraph{Proof irrelevance and homotopy type theory}
During his master's internship supervised by Matthieu Sozeau, Philipp
Haselwarter studied a formulation of proof-irrelevance based on the
decomposed presentation of CIC by Spiwack and Herbelin
\footcite{DBLP:conf/types/HerbelinS13}. Following this work, Gaëtan Gilbert,
Nicolas Tabareau and Matthieu Sozeau developed the theory and
implementation of \emph{strict} or definitionally proof-irrelevant
propositions in the Calculus of Inductive Constructions. In
collaboration with Jesper Cockx (Chalmers), they developed this notion
in full in an article presented at POPL 2019
\cite{gilbert:hal-01859964}.
\paragraph{Dependent pattern-matching and recursion}
Cyprien Mangin and Matthieu Sozeau developed a complete rewriting of the
\Equations plugin which provides a high-level interface for the
definition of mutual, nested and well-founded recursive definitions
using dependent pattern-matching in Coq, without axioms. The tool also
derives useful reasoning principles on these definitions, significantly
raising the scope of definitions handled by previous tools
(\textsc{Function} and \textsc{Program}), and turning Coq into a viable
alternative to its cousins Agda and Idris for dependently-typed
programming. Developing this new version of \Equations was a
significant engineering effort that spanned the whole evaluation
period. An earlier version of the system was presented at LFMTP 2015
\cite{mangin:hal-01248807} and an article describing the latest version
is in revision~\cite{mangin:hal-01671777}.
An alternative simplification of dependent pattern-matching avoiding
the use of equalities and resulting in smaller proof terms is being
implemented by Thierry Martinez, following the PhD thesis work of Pierre
Boutillier and the internship work of Meven Bertrand. The algorithm
based on small inversion and generalisation is the object of a paper to
be submitted to the TYPES post-proceedings.
\paragraph{Unification}
Matthieu Sozeau worked in collaboration with Beta Ziliani (PhD at
MPI-Saarbrücken, now assistant professor at Córdoba, Argentina) on
formalising the unification algorithm used in Coq, a central component
of type-checking and tactical reasoning in the proof assistant, with which
the user interacts all the time. This resulted in a precise formalisation of
all the rules of unification including the ones used for canonical
structure resolution and universes, presented in a manner accessible to
users (work presented at ICFP 2015~\cite{ziliani:hal-01248804} and refined into a journal
article~\cite{ziliani:hal-01671925}).
\paragraph{Certified compilation and meta-programming}
MetaCoq\footnote{\url{http://metacoq.github.io/metacoq}} is a project
led by Matthieu Sozeau, in collaboration with Simon Boulier and Nicolas
Tabareau in Nantes, Abhishek Anand and Gregory Malecha (BedRock Systems,
Inc) and Yannick Forster in Saarbrucken. The project extends the
Template-Coq reification plugin of Malecha with specifications of the
typing rules and basic metatheoretical properties of the system, a
reference type checker for Coq, written in Gallina, an
implementation of extraction and a monad for programming deeply embedded
plugins in Coq itself, in the style of MTac. The foundation of this
project was presented at ITP 2018~\cite{anand:hal-01809681}, and a
journal article is in preparation.
Matthieu Sozeau participates to the CertiCoq
project\footnote{\url{https://www.cs.princeton.edu/~appel/certicoq}} led
by Andrew Appel at Princeton Univ., whose aim is to verify a
compiler from Coq's Gallina language down to CompCert C-light which
provides itself a certified compilation path to assembly
language. Matthieu Sozeau authored the front-end part of CertiCoq
including extraction, integrated in MetaCoq, along with another phase.
The CertiCoq team expects to release a first version of the compiler in
the beginning of 2019, along with an article describing it.
In collaboration with Jan-Oliver Kaiser (MPI-SWS), Beta Ziliani
(CONICET/FAMAF), Robbert Krebbers (ICIS) and Derek Dreyer (MPI-SWS),
Yann Régis-Gianas participates in the Mtac2 project, a shallowly
embedded metaprogramming language for Coq. The new version of this
language has been presented at ICFP 2018~\cite{kaiser:hal-01890511}. It
includes in particular a dependently-typed variant of the LCF tactic
typing discipline. In collaboration with Xavier Denis (Univ. Paris
7), Yann Régis-Gianas is implementing a compiler for Mtac2.
\paragraph{Extensionality and Intensionality in Type Theory}
Théo Winterhalter, Nicolas Tabareau and Matthieu Sozeau studied and
formalised a complete translation from Extensional to Intensional Type
Theory in Coq, that was presented at CPP 2019
\cite{winterhalter:hal-01849166}. Using the MetaCoq framework, this
establishes formally that only the Functional Extensionality and
Uniqueness of Identity Proofs principles are necessary to effectively
embedd ETT in ITT.
\paragraph{Equivalences for free!}
Nicolas Tabareau (Inria Nantes), Eric Tanter (Univ.\ Chile in Santiago) and
Matthieu Sozeau developed a new parametricity translation for justifying
the transport of programs and proofs by equivalences in type theory (work presented at ICFP 2018~\cite{tabareau:hal-01559073}, see Section 1).
% The main difficulty is to show that
% every construction of type theory (minus inductive families indexed by
% universes) respects type equivalence, and to provide a modified
% parametricity translation that can be used to construct the proof of
% invariance by equivalence of any term, avoiding the introduction of
% transports. This translation is instrumented using type classes so that
% one can automatically transport libraries of implementations and their
% proofs from one type to an equivalent one, including cases where
% dependent types are used, improving on existing solutions for transfer
% like CoqEAL~\footcite{cohen:hal-01113453}.
\paragraph{Development of Coq}
The amount of contributions to the Coq system increased significantly in
the recent years. Hugo Herbelin, Matthieu Sozeau and Théo Zimmermann,
helped by members from Gallinette (Nantes) and Marelle
(Sophia-Antipolis), devoted an important part of their time to
coordinate the development, to review propositions of extensions of Coq
from external and/or young contributors, and to propose themselves
extensions. During the evaluation period, versions 8.5 through 8.9 of
Coq were released (see Section 3 for more details).
\paragraph{Software engineering aspects of the development of Coq}
Théo Zimmermann has studied software engineering and open collaboration
aspects of the development of Coq. In collaboration with Annalí
Casanueva Artís from the Paris School of Economics, he studied the
migration of the Coq bug tracker from BugZilla to github. The results
show an increased number of bugs by core developers and an increased
diversity of the people commenting bug reports, and validate
{\em a posteriori} the usefulness of such a switch. A paper
\cite{zimmermann:hal-01951176} was presented at the EAQSE workshop.
Théo Zimmermann has founded the coq-community GitHub organisation in
July 2018. This is a project for a collaborative, community-driven
effort for the long-term maintenance and advertisement of Coq
packages. Théo Zimmermann and Yann Régis-Gianas are preparing an article
of the model proposed by the various existing *-community GitHub
organisations.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Collaborations}
% {\footnotesize\sl List the partners with whom you had a strong and fruitful collaboration during the evaluation period (joint publications, joint software development) and refer to the topic and the outcome of the collaboration. TBR}
Matthieu Sozeau is a participant in the ERC CoqHoTT led by Nicolas
Tabareau and the CertiCoq project led by Andrew Appel at Princeton
Univ. since 2015.
Andrej Bauer (Univ. of Ljubljana) visited $\pi r^2$ and PPS for one
month in September 2015 to collaborate with Matthieu Sozeau and Philipp
Haselwarter on the subject of proof irrelevance and squash
types. Phillip Haselwarter went on to do a PhD with Bauer.
Beta Ziliani (Univ. of Córdoba) is a long time collaborator of both
Matthieu Sozeau and Yann-Régis Gianas on the topics of unification
(ICFP 2015, JFP 2016) and tactic languages (ICFP 2018).
Amin Timany (KU Leuven, Belgium) visited the team for two months in
March-April 2017 and collaborated with Matthieu Sozeau on the design and
implementation of cumulative inductive types in Coq throughout 2017-2018.
Vadim Zaliva (PhD student at CMU) visited the team for one month in July
2018 and collaborated with Matthieu Sozeau on the use of Template-Coq to
verify translations from shallow to deep embeddings (publication at
CoqPL 2019).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{External support}
% {\footnotesize\sl List the various support you had, e.g. Inria project labs, national initiatives (ANR, PIA, etc), European and international projects, industrial contracts. This subsubsection must be very short. Details should be provided in section \ref{finance}. TBR.}
The work on this axis was partly supported by the ERC CoqHoTT. Coq
development was supported by an Inria ADT and specific support from Inria's DGD-T.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Self assessment}
% {\footnotesize\sl Outline the strong and the weak points. What should be continued, modified, stopped? TBR.}
The development of the core type theory of Coq continued with the
addition of a more sophisticated universe system and the introduction of
strict propositions, which clearly benefit to users. However, we are
currently lacking ways to ensure without a doubt the consistency of
these extensions and the safety of the implementation. We should prioritise
the verification of the implementation of Coq's kernel and the
metatheoretical study of its type system using MetaCoq.
Unfortunately, two PhD students preferred to leave for industry before
completing their thesis. In a somewhat related vein, the
increasing demanding activity on Coq is quite time-consuming for some members of the team, despite the improvement of the engineering support for Coq.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Miscellaneous results}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
This subsection lists the results achieved by the team in other directions than the five research axes.
\paragraph{Proofs and surfaces}
Following ideas of Richter-Gebert, Pierre-Louis Curien, together with Jovana Obradović (while on her postdoc in Prague), joined a project with Zoran Petrić and other Serbian colleagues on formalising proofs of incidence theorems (arising by repeated use of Menelaus theorem) by means of a cyclic sequent calculus, which has been proved sound and been experimented on an extended set of examples from elementary projective geometry. A paper is being written.
% Here, a (proof of a) sequent $\vdash \Gamma$ stands for the conjunction of all (proofs of) traditional sequents $\Gamma\setminus \psi\vdash \psi$. We have designed a proof system, showed its soundness,
\paragraph{Hofstadter nested recursive functions and Coq}
Pierre Letouzey has been studying a family of nested recursive
functions proposed by Hofstadter,
%in his book ``Gödel Escher Bach'',
see \url{https://oeis.org/A005206} and
\url{https://oeis.org/A123070}. Some new results have been proved in
Coq and presented in ~\cite{letouzey:hal-01195587}. A generalisation of this work is
ongoing,
%already bringing a large number of new insights as well as
%many new conjectures. A large part of this follow-up is already certified in
%Coq, with generalised and/or nicer proofs,
see
\url{https://www.irif.fr/~letouzey/hofstadter_g/}. Many points
remain to be explored, like the surprising occurrence of a Rauzy
fractal during the investigations,
see \url{https://www.irif.fr/_media/rencontres/pps2018/letouzey.pdf}.
\paragraph{Real Numbers in Coq}
The present Coq library of real numbers is made of 17 axioms. Daniel de Rauglaudre has been studying the possibility of making an implementation with one only axiom: the Limited Principle of Omniscience (LPO), which says that we can differentiate an infinite sequence of~$0$s from an infinite sequence holding something else than~$0$
%cannot be proved in constructive logic).
This axiom had been already used in the formal proof of Puiseux' theorem done some years ago (only axiom of this proof too).
%
Real numbers are defined by an infinite sequence of digits and the operations of addition and multiplication by algorithms using LPO.
%
It was tested in OCaml, the axiom being replaced by a function having a limit corresponding to the precision of the computation and it seems to work. But the proof in Coq that this implementation is a field stumbles on difficulties about the associativity of addition which is more complicated to establish than expected.
%Several tracks have been experimented with Hugo Herbelin's help.
\paragraph{Proofs of algorithms on graphs}
Jean-Jacques Lévy and Chen Ran (PhD student, Institute of Software, Beijing) pursue their work about formal proofs of graph algorithms. %Their goal is to provide proofs of algorithms checked by computer and human readable.
%While these kinds of proofs exist for algorithms on inductive structures or recursive algorithms on arrays, they seem less easy to design for combinatorial structures such as graphs.
In 2016, they completed proofs for algorithms computing the strongly connected components in graphs (Kosaraju 1978 and Tarjan 1972). This work was done using
%Their proofs use the multi-sorted first-order logic with inductive predicates of
the Why3 system (team Toccata, Saclay) and the numerous automatic provers interfaced with Why3. A very minor part of these proofs is also achieved in Coq. The difficulty of this approach is to combine automatic provers and the intuitive design, and to find the good level of abstraction in order to avoid too many implementation features while keeping an effective presentation.
In 2017, the same proofs were fully completed in Coq-SSReflect with the Mathematical Components library by Cohen and Théry (team Marelle, Sophia-Antipolis), and in Isabelle-HOL by Merz (team VeriDis, Nancy), both proofs with the assistance of Jean-Jacques Lévy. These proofs are between a factor~3 to~8 in length with respect to the initial Why3 proofs
%, but more importantly they look less human readable, mainly because of the absence of automatic deduction and several technicalities about termination.
On the way, this collaboration led to a new, better presentation of the Why3 proof. These works were presented at
%
%Part of this work (Tarjan 1972) was presented
JFLA 2017,
%a more cmprehensive version was presented at the
at VSTTE 2017 in Heidelberg, and a paper is under submission.
Scripts of proofs can be found at \url{http://jeanjacqueslevy.net/why3}, where other proofs of graph algorithms are also presented: acyclicity test, articulation points, biconnected components. A proof of Tarjan's planarity test is also under design.
%A paper entitled ``Formal Proofs of Tarjan's Algorithm in Why3, Coq and Isabelle'' is under submission to a conference.
\paragraph{Detecting \texorpdfstring{$\mathbf{k}$}{k}-synchronisability violations}
As part of the research program of the Inria-CAS project VIP,
Ahmed Bouajjani (Univ.\ Paris~7), Constantin Enea (Univ.\ Paris~7), Kailiang Ji and Shaz Qadeer (Microsoft Research)
% introduced a bounded analysis that
%explores a special type of computations, called $k$-synchronous, for analysing message passing
programs
gave a procedure for deciding \emph{$k$-synchronisability} of a program, i.e.\ whether
every computation is equivalent (has the same happens-before relation) to one of its $k$-synchronous
computations. They also showed that reachability over $k$-synchronous computations and checking $k$-synchronisability are both PSPACE-complete~\cite{bouajjani:hal-01947855}.
%Furthermore, they introduced a class of programs
%called \emph{flow-bounded} for which the problem of deciding whether there exists a~$k>0$ for which
%the program is $k$-synchronisable, is decidable. The \emph{$k$-synchronisability} violation detection
%algorithm was implemented in Spin model checker.
%This work was presented at CAV 2018.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Evolution of research directions during the evaluation period}
%{\footnotesize\sl Recall briefly (1 page max) the objectives that were given on the
%occasion of the last evaluation of the project (or for its creation). TBR.}
%
%{\footnotesize\sl Comment the research activity of the evaluation period
%with respect to the objectives above. For example, an objective could have been canceled or
%postponed due to technical difficulties or to the departure of a team
%member. Or, new research directions could have emerged. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
We comment on the objectives planned in the 2015 evaluation report of the team.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Effects in proof theory and programming}
\paragraph{Effects in proof theory}
Beside the question of the strength of classical realisability, we
addressed all our objectives, though, unfortunately, in large part due
to the increasing activity on Coq, without always having enough time
to concentrate on finalising a paper out of our results.
%% The objective of characterising a type theory internalising the full
%% intensional axiom of choice and the independence of premises has been
%% realised by Pierre-Marie Pédrot and Nicolas
%% Tabareau~\footcite{PedrotTabareau18} while Pierre-Marie Pédrot was a postdoc.
%% We made a short proof of a reformulation of the negation of the
%% continuum hypothesis in type theory (work to be written).
%% We did not have time to investigate in depth the use of side-effects in
%% well-ordering of real numbers.
%% Étienne Miquey developed a calculus mixing classical logic and
%% dependencies~\cite{miquey:hal-01375977} and
%% resolved~\cite{miquey:tel-01653733} a conjecture left open
%% in~\footcite{Herbelin12}. We did not give a final answer to the
%% question of the logical strength of classical realisability, but we
%% have some hints on how to proceed.
%% We refined our investigations on normalisation-by-evaluation as a
%% computational content for logical completeness proofs, but did not have
%% time to put a conclusion to this work. We have a paper in journal
%% format almost complete relating exceptions to Coquand-Hofmann's
%% extension of Friedman's $A$-translation. We have an incomplete draft
%% paper and we made several talks about relating memory assignments to
%% Kripke's and Cohen's forcing translations. We stumbled upon finding the
%% conditions for computational iterated forcing to be consistent, and on
%% the strength of forcing in the absence of control. However, by trying
%% to answer these questions, we started to investigate a promising
%% general theory of monadic and comonadic effects in logic.
\paragraph{Lazy evaluation and its dual} Theoretical studies say that there is a
dual to lazy evaluation and it remains interesting to evaluate whether
there exist effective incarnations of it in the wild. We however did
not make progresses on this question.
\paragraph{Game semantics of lazy evaluation} We did not explore game semantics
of lazy evaluation, which was a relatively marginal point in our
project.
%% However, it may come almost automatically from the
%% continuation-passing-style interpretation of lazy evaluation, since
%% continuation-passing-style targets a polarised calculus and game
%% semantics is mainly about moving from an intensional presentation of
%% polarised calculi to an extensional one.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Reasoning and programming with infinite data}
\paragraph{Infinite proofs, fixed point logics and coinductive reasoning: syntax and semantics}
In this direction, the efforts were put on the development of a syntax and semantics for fixed-points and infinitary logics, where the results we obtained go far beyond our original expectations.
With respect to copatterns and coequation, the dependently-typed case was not addressed, but some implementation was developed instead as reported above.
\paragraph{Automata theory meets proof-theory}
Original plans were to develop a framework for non-determinism in Ludics and to lift the existing framework for deterministic finite automata and formal languages in computational ludics to non-deterministic finite automata and $\omega$-automata. Some investigations in the early phase of Amina Doumane's PhD showed that the problem was much more complex than expected (both in the treatment of existential non-determinism and in expressing the $\omega$-acceptance condition in a way that is compatible with the technical setting under consideration). The research effort in connecting automata theory and proof-theory was therefore reoriented towards the development of the non-wellfounded proof-theory of the linear-time $\mu$-calculus and the refinement of classical relationships between LT$\mu$-calculus and automata, in order to design a new, constructive proof of completeness of the $\mu$-calculus.
\paragraph{Functional reactive programming}
While proof systems for LTL and type systems for FRP were indeed investigated in Rémi Nollet's Master and early PhD work and in Amina Doumane's PhD, the denotational semantics of FRP has not yet been addressed and is still in plans for future works.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Effective higher-dimensional algebra}
\paragraph{Algebraic methods for the word problem}
The improvement of the Knuth-Bendix completion started with~\cite{dehornoy:hal-01141226}, which established a theoretical setting to transfer methods from Garside theory to rewriting; this led to the ongoing development of the new KGB completion procedure, enhanced with elements of Garside theory.
%
We planned a generalisation of the connexion between convergent presentations and the word problem for monoids, based on~\footcite{OttoKatsuraKobayashi98}; we supervised two M2 interns on this theme, but the students did not pursue in PhD.
\paragraph{Improvement of the homotopical completion-reduction procedure}
An unforeseen hitch arose while developing rewriting theory in a linear setting, and took much of our energy: indeed, the article~\cite{guiraud:hal-01006220} on rewriting methods for associative algebras was considered finished at the previous evaluation, but contained a gap in a proof that finally induced three more years of work.
Cubical polygraphic resolutions were studied by the PhD thesis of Maxime Lucas~\cite{lucas:tel-01668359}, who went way further than the initial expectations in the understanding of the cubical setting and the development of effective computational methods.
The link between confluence monoids and resolutions was investigated by the PhD thesis of Cyrille Chenavier~\cite{chenavier:tel-01415910}, leading to more effective methods than planned; he also worked on several other related themes, mostly around an algebraic account of completion.
The planned work on Steiner theory was quickly cancelled, after a theoretical obstruction was found.
% However, recent progress by Henry and Hadzihasanovic on ``regular polygraphs'' might lead to resume this objective in a more restrictive setting.
%
The investigation on higher homotopical reduction was harder than expected, but an article containing the first results in this direction is almost finished.
\paragraph{Weak higher-dimensional categories}
We made mild progress on the coherence of weak higher categories during the PhD thesis of Maxime Lucas~\cite{lucas:tel-01668359}, who studied the coherence of weak natural transformations; an ongoing collaboration with Marcelo Fiore is expected to provide new insights thanks to the point of view of $n$-oidal categories.
%
The interaction with homotopy type theory is the main subject of the recently started PhD thesis of Antoine Allioux, although with a different point of view than planned, where opetopes replace cubes as the basic blocks of higher structures. This line of work should connect with the syntactic work on opetopic sets reported above.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Incrementality}
\paragraph{Incremental computing based on differential functional programming}
We consider the computational model for differential functional
programming to be stabilised now and hence this objective to be
fulfilled.
\paragraph{Certifying incremental computation}
The cache-transfer-style static differentiation has been proved
correct in Coq. The next challenge is to equip this
functional programming language with a proof system to be able to
prove properties about incrementalised programs, especially about
their execution costs and their asymptotical complexity.
\paragraph{Differential semantics}
As a result of Girka's PhD thesis, we already have a usable formal
framework to reason about semantic differences of programs. We want to
know if it can scale up to more realistic programming languages.
\paragraph{Certified incremental proof-checking}
There is no significant progress on this objective, because we focused
on certifying incremental programs.
This direction is simply postponed.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Metatheory and development of Coq}
\paragraph{Monadic effectful programming in Coq}
Our study of Coq extensions using monadic approaches has started with
the work about simulable monads and certified interactive
computations. Unexpectedly, it has continued with Mtac2 and with
FreeSpec. Because we dedicated our time to these last two important
results, we postponed our specific plan to look for more efficient
computational models to execute programs based on simulable
monads. This investigation is simply postponed and could actually
benefit from recent advances about algebraic effects to enable a
closer interaction between efficient untrusted oracles and less
efficient certified validators.
\paragraph{Typed tactics}
With Mtac2, we consider that the objective to legitimate Mtac as a
credible alternative to Ltac is achieved.
%
The goal to get efficient tactics by means of compilation is an active
research project and should lead to a practical implementation very
soon.
%
A last goal we had in mind was to explore domain specific proof
script languages. This has not yet been considered, essentially
by lack of time.
\paragraph{Equality in type theory}
The objective of relating typed and untyped intensional equality in the presence of
subtyping did not see progress during the evaluation
period, as we focused on other items.
The work on strict propositions~\cite{gilbert:hal-01859964}
directly addresses the objective about proof-irrelevance in Coq, providing a definitional proof-irrelevant sort in Coq.
An ongoing work of Antoine
Allioux, Eric Finster, Yves Guiraud and Matthieu Sozeau on the definition of coherent
higher-dimensional structures in type theory addresses the main
obstacle in the objective of understanding coherent structures in type theory.
In the direction of capturing fragments of extensional equality, the work of
Théo Winterhalter, Matthieu Sozeau and Nicolas Tabareau~\cite{winterhalter:hal-01849166} on
an effective translation from extensional to intensional type theory
allows for the inclusion of extensional equality in type theory, by
translation. % However we did not manage to capture only fragments of
% extensional reasoning: the global translation requires the
% full Uniqueness of Identity Proofs (UIP) principle at every type.
In the course of this investigation, it appeared that restricting the
reflection rule to particular types for which UIP is provable is not
enough to prevent UIP at every type, making the idea of restricting
extensionality to a fragment (in a $1$-level type theory) dubious.
Our work on formalising the unification algorithm of
Coq is an important step in providing a formal underpinning to this
central part of the proof assistant. We plan to pursue the second part
of mechanising the unification algorithm in Coq as part of the MetaCoq
project (new objective).
The new version of \Equations addresses the objective of permitting definitions by
pattern-matching using definitional or propositional versions of the UIP principle
on the concerned types. The tool was also greatly generalised to
handle complex recursion schemes (new objective).
\paragraph{Coq as a general-purpose platform for certified proofs}
The main objective here was to open up the development process and
modularise the architecture of the system, so that it can be more easily
maintained and extended. As described previously in this report, the
development model of Coq substantially changed during the evaluation
period, allowing more developers to contribute and work concurrently on
the system. While our objective of modularisation is not yet attained, a
number of efforts go into this direction: functionalisation and
isolation of interfaces and components, deprecation of redundant
components, and, in general, higher requirements on the quality of the code
being integrated. The management, development and maintenance of software of this size, with around a dozen core
developers and a growing number of external contributors, is a huge effort. We are thankful for
Inria's help in recruiting two engineers through the Coq consortium that
are focusing on these tasks.
Nevertheless, the overall increase of the programming and coordinating activity
on Coq took up a lot of the time of the members of the team involved
in the development.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Knowledge dissemination}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Publications}
%{\footnotesize\sl This section should count the publications of the project-team during the evaluation period. A bibliography at the end of this document (sorted by category), should list in extenso all the publications denoted here. The project-team will select a few ``major'' publications that will be available on the evaluation seminar web site. Length: max 1.5 page. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{center}
\begin{tabular}{|l|r|r|r|r|} \hline
& 2015 & 2016 & 2017 & 2018+ \\ \hline \hline
PhD Theses & 2 & 2 & 4 & 2 \\ \hline
H.D.R.~(*) & & & & 1 (Spring 2019) \\ \hline
Journals & 6 & 7 & 15 & 9 \\ \hline
Conference proceedings (**) & 8 & 3 & 6 & 7 \\ \hline
Book chapters & 1 & & & 1 \\ \hline
%Books (written) & & & & \\ \hline
%Books (edited) & & & & \\ \hline
%Patents & & & & \\ \hline
%General audience papers & & & & \\ \hline
Technical reports & 1 & 1 & 1 & \\ \hline
\end{tabular}
\smallskip
(*) Habilitation à diriger des recherches\\
(**) Conferences with a program committee
\end{center}
The most important journals for the team are (number of accepted papers in parentheses):
\begin{itemize}
\item Journals in theoretical computer science or logic, such as:
Journal of Formalized Reasoning~(1),
Journal of Functional Programming~(1),
Journal of Symbolic Computation~(1),
Journal of Symbolic Logic~(1),
Logical Methods in Computer Science~(1),
Mathematical Structures in Computer Science~(3),
Proceedings of the ACM on Programming Languages~(3).
\item Mathematical journals with a general audience, such as:
Advances in Mathematics~(2),
Compositio Mathematica~(1),
Mathematische Zeitschrift~(1).
\item Mathematical journals specialised in algebra and topology, such as:
Algebras and Representation Theory~(1),
International Journal of Algebra and Computation~(1),
Journal of Homotopy and Related Structures~(1),
Journal of Pure and Applied Algebra~(1),
Journal of Topology~(1).
\end{itemize}
\smallskip
The top two conferences in our themes are
Principles of Programmming Languages~(1) and
Logic in Computer Science~(2).
%
Other important conferences include:
Certified Programs and Proofs~(2),
Computer Science Logic~(1),
European Symposium on Programming~(2),
Formal Structures for Computation and Deduction~(2),
Foundations of Software Science and Computation Structures~(2),
Interactive Theorem Proving~(1),
International Conference on Functional Programming~(1)
Principles and Practice of Declarative Programming~(2).
\subsection{Software}
%{\footnotesize\sl Provide a short description of advanced software.
%Use the criteria for software self-assessment of Inria's Commission
%d'Evaluation, available at
%\url{http://www.inria.fr/en/content/download/11783/409884/version/4/file/SoftwareCriteria-V2-CE.pdf}.
%How are they distributed? Under what kind of license?
%What is their impact? Does there exist competitors? Refer to
%benchmarks if applicable.
%Give the URL of a Web site describing the software system.
%Length for each software: depending on the software maturity and advancement, max 1/2 page per software. TBR.}
%%%%%
\paragraph{Coq} An interactive proof assistant based on type theory.
Web site: \url{http://coq.inria.fr}. Self-assessment:
\begin{itemize}
\item Audience:
A-5 (wide audience, large user's community).
\item Software originality:
SO-4 (original software implementing a fair number of original ideas).
\item Software maturity:
SM-4 (major software project, strong software engineering).
\item Evolution and maintenance:
EM-4 (well-defined and implemented plans for future maintenance and evolution).
\item Software distribution and licensing:
SDL-4/5 (public source or binary distribution on the Web). Binary
packages available for common platforms.
\end{itemize}
Coq~8.5 final was relased in January 2016, followed by~8.6 (December 2016), 8.7 (October 2017), 8.8 (April 2018) and~8.9 (February 2019). Among many fixes and improvements, these versions bring:
\begin{itemize}
\item Better performance and stability, along with cleanups of the
interfaces of the system.
\item Stabilisation and improvements of asynchronous document processing
and compilation, universe polymorphism, the new proof engine and many
tactics.
\item Integration of the SSReflect plugin providing a proof language
centered on small-scale reflection.
\item Better tool support for deprecation, control of warnings, and
building of contributions and plugins.
\item A collaborative migration of the documentation to the Sphinx tool
allowing easier community improvements.
\end{itemize}
During these four years, the development of Coq moved to an entirely
decentralised, collaborative model. We set up procedures for
contributing and a formal review process along with a move to modern
software engineering tools: using github for code, pull requests,
reviews and issues, and setting up a thorough continuous integration
system. It attracts now dozens of external contributors and has a
fast-paced development cycle. As such, Coq is probably the most widely
used and developed proof assistant on the market. Coq is gradually
moving towards an industry-strength tool, compared to its direct
competitors Lean and Agda, as attests its continued use for large
verification projects. The NSF DeepSpec Expedition project is such an
example: its aim is to formalise and connect specifications of a full
stack from hardware to OS to user-level software in Coq.
%%%%%
\paragraph{\Equations}
A plugin for Coq elaborating high-level recursive function
definitions using dependent pattern-matching to Coq's kernel type
theory.
Web site: \url{http://mattam82.github.io/Coq-Equations/}. License: LGPL 2.1. Self-assessment:
\begin{itemize}
\item Audience:
A-4 (large audience, used by people outside the team).
\item Software originality:
SO-4 (original software implementing a fair number of original ideas).
\item Software maturity:
SM-3 (well-developed software, good documentation, reasonable software engineering).
\item Evolution and maintenance:
EM-3 (good quality middle-term maintenance).
\item Software distribution and licensing:
SDL-4 (public source or binary distribution on the Web).
\end{itemize}
\Equations competitors are the Agda and Idris dependently-typed
programming languages which provide similar functionality albeit without
the verification guarantees of an elaboration, and the Function
definition packages of Lean and Isabelle/HOL. The first production-ready
version was released in December 2017 and initial feedback from users is
encouraging.
%%%%%
\paragraph{Rewr}
A prototype of computer algebra system, using rewriting methods to compute resolutions and homotopical invariants of monoids. The library implements various classical constructions of rewriting theory (such as completion), improved by experimental features coming from Garside theory, and allows higher algebra computations based on Squier theory. Specific functionalities have been developed for usual classes of monoids, such as Artin monoids and plactic monoids.
Web site: \url{http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/rewr}. Self-assessment:
\begin{itemize}
\item Audience: A-3 (ambitious software, usable by people outside the team).
\item Software originality: SO-4 (original software implementing a fair number of original ideas).
\item Software maturity: SM-2 (basic usage works, terse documentation).
\item Evolution and maintenance: EM-3 (good quality middle-term maintenance).
\item Software distribution and licensing: SDL-4 (public source or binary distribution on the Web).
\end{itemize}
%%%%%
\paragraph{Catex}
A Latex package and an external tool to typeset string diagrams easily from their algebraic expression. Catex works similarly to Bibtex.
Web site: \url{https://www.irif.fr/~guiraud/catex/catex.zip}. Self-assessment:
\begin{itemize}
\item Audience: A-2 (used by people in the team or close to the team).
\item Software originality: SO-4 (original software implementing a fair number of original ideas).
\item Software maturity: SM-3 (well-developed software, good documentation, reasonable software engineering).
\item Evolution and maintenance: EM-3 (good quality middle-term maintenance).
\item Software distribution and licensing: SDL-4 (public source or binary distribution on the Web).
\end{itemize}
%%%%%
\paragraph{Cox}
A Python library for the computation of coherent presentations of Artin monoids, with experimental features to compute the first dimensions of the Salvetti complex.
Web site: \url{https://www.irif.fr/~guiraud/cox/cox.zip}. Self-assessment:
\begin{itemize}
\item Audience: A-1 (internal prototype).
\item Software originality: SO-3 (original software reusing known ideas and introducing new ideas).
\item Software maturity: SM-2 (basic usage works, terse documentation).
\item Evolution and maintenance: EM-1 (no real future plans).
\item Software distribution and licensing: SDL-4 (public source or binary distribution on the Web).
\end{itemize}
%\yves{Si besoin, le modèle est en commentaire ici (ne pas l'effacer !)}
% \paragraph{Name of software}
% {\footnotesize\sl Short description. TBR.}
% Web site: \url{http://XXXX}. Self-assessment:
% {\footnotesize\sl Delete the lines that are not appropriate,
% leaving only the appropriate characterisation. Update the
% comments in parentheses if needed for a more precise characterisation.
% TBR.}
% \begin{itemize}
% \item Audience:
% A-1 (internal prototype).
% A-2 (used by people in the team or close to the team).
% A-3 (ambitious software, usable by people outside the team).
% A-4 (large audience, used by people outside the team).
% A-5 (wide audience, large user's community).
% \item Software originality:
% SO-1 (none).
% SO-2 (minor contributions to existing software, reusing known ideas).
% SO-3 (original software reusing known ideas and introducing new ideas).
% SO-4 (original software implementing a fair number of original ideas).
% \item Software maturity:
% SM-1 (demos work, loose documentation).
% SM-2 (basic usage works, terse documentation).
% SM-3 (well-developed software, good documentation, reasonable software engineering).
% SM-4 (major software project, strong software engineering).
% SM-5 (high-assurance software, certified by an evaluation agency or formally verified).
% \item Evolution and maintenance:
% EM-1 (no real future plans).
% EM-2 (basic maintenance to keep the software alive).
% EM-3 (good quality middle-term maintenance).
% EM-4 (well-defined and implemented plans for future maintenance and evolution).
% \item Software distribution and licensing:
% SDL-1 (none).
% SDL-2 (privately distributed within the close community).
% SDL-3 (distributed to industrial partners in a contractual setting).
% SDL-4 (public source or binary distribution on the Web).
% SDL-5 (external packaging and distribution, as part of a popular open
% source distribution or a commercially-distributed product).
% \end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Technology transfer and socio-economic impact}
% {\footnotesize\sl Please describe your activities that have had a
% socio-economic impact. Note that this is not limited to industrial
% transfer, although it is clearly included. Provide a short
% description of each activities :
% 1) What kind of action are/were you involved in? Was it a punctual action or continual one?
% 2) Under what conditions, in what framework, was
% the action done ?
% 3) Who are the targeted end users? Who were your interlocutors?
% 4) What were the major steps? What was the involvement of your team ?
% 5) From your viewpoint, have you reached your objective? What is the real impact? Length : depending on the team activities, this subsection should range between 1/3 and 3 pages. TBR}
The team did not undertake a sustained action of transfer, however the
impact of Coq in industry is starting to show and we have informal
contacts with industry users. In particular, we know of uses of Coq at
Intel (Michael Soegtrop is a regular Coq contributor),
Tweag I/O (Arnaud Spiwack is a close collaborator), Mitsubishi,
Facebook, Google (collaborators of Adam Chlipala's group at MIT),
the FireEye company (which hired a team of Coq proof engineers on a
cyber-security project, now cancelled), BedRock Systems Inc.\ (which
employs Gregory Malecha, a collaborator of Sozeau), and Edukera (a French
company whose goal is to bring proof assistants to the classroom), among
others. Our hope is that the Coq consortium, a structure meant to
organise the Coq community of users from academia and industry can
ultimately undertake potential technology transfer activities. Its
setup, pushed mainly by Yves Bertot and Maxime Dénès in the Marelle
team, has however encountered administrative difficulties until now. Due
to the completely open source nature of Coq, however, this did not
actually prevent industrial uses of the system.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Teaching}
% {\footnotesize\sl
% Indicate the number of hours spent in teaching activities
% on a yearly basis for each scientific staff member, where the teaching
% activities were carried out (Universities - Licence, Master's -,
% Engineering schools). Length : max 1 page. TBR.}
% {\footnotesize\sl
% \noindent
% Indicate the relationships with doctoral programs and state precisely
% the nature of these relationships. TBR.}
%%%%%
\paragraph{Research master courses (from 10 to 30 hours per course)}
Pierre-Louis Curien taught every year in the MPRI Master~2 course ``Models of programming languages: domains, categories, games'' (together with Thomas Ehrhard and Paul-André Melliès).
He taught courses on homotopy type theory, and on the Foundations of Programming Languages at East China Normal University (ECNU), Shanghai (June 2017 and November 2018).
Yves Guiraud taught a course on the applications of rewriting methods in algebra in the Master~2 Mathématiques Fondamentales of Lyon (January~2017).
Hugo Herbelin taught a class at the LMFI Master~2, entitled ``Preuves et
programmes en logique classique'' in 2015, 2016 and 2017 (48h each
year) and on homotopy type theory in 2018 (24h, collaboration with
Nicolas Tabareau).
Since 2015, Pierre Letouzey has taught two courses to the LMFI Master~2 students: ``Introduction to computer-aided formal proofs'', and an
introduction to programming, initially in OCaml, now in Coq (48h per
year).
Pierre Letouzey and Matthieu Sozeau were lecturers
at the ``École de Printemps d'Informatique Théorique'' on ``Preuves mécanisées de programmes'' in
Fréjus in May 2015.
Yann Régis-Gianas took part every year in the MPRI Master~2 course entitled ``Type
systems'': he gave lectures about
generalised algebraic data types, higher-order Hoare logic and
dependently-typed programming.
Alexis Saurin taught, jointly with Christine Tasson, an LMFI Master~2 course entitled ``Outils classiques pour la correspondance preuves-programmes'' in 2015-2016 and in 2018-2019. In 2016-2017 and 2017-2018, he taught the Master~2 course entitled ``Cours fondamental de logique: théorie de la démonstration''.
%
He chaired the LMFI Master~2 from 2013 to 2018.
Matthieu Sozeau taught the MPRI Master~2 course on ``Advanced uses of proof
assistants'' for the whole 2015-2019 period with Bruno Barras (Inria
Deducteam), 12h/year. He gave a guest lecture on dependent
pattern-matching and \Equations at the Univ. of Saarland in April
2018, and an introductory lecture on dependent type theory at the
EUTYPES summer school in Ohrid, Macedonia, in August 2018. He taught a
course at the EJCP 2017 summer school in Toulouse in June 2017 and at
EJCP 2018 in Lyon in July 2018, on an introduction to interactive theorem
proving.
%%%%%
\paragraph{Other teaching}
Pierre Letouzey's regular duty as teacher in the Computer Science
department of Univ. Paris~7 amounts to 192h per year. Since 2015, Pierre Letouzey
taught in particular ``Compilation'' to Master~2-Pro students (50h/year) and
``Computed-aided formal proofs'' to Master~1 students (36h/year).
Yann Régis-Gianas performed the same amount of teaching hours (except
in 2018 and 2019 because he obtained a
part-time sabbatical funded by INRIA). He is usually responsible for
the Master~1 course ``Compilation'' (50h/year), for the Master~2~Pro course
``Comparative programming'' (50h/year) and for the Master~2-Pro course
``Advanced Concepts in Object Oriented Programming''
(36h/year).
%%%%%
\paragraph{Internship supervision}
Pierre-Louis Curien supervised Akira Yoshimizu, who had a six-month
INRIA international internship (Nov.\ 2014 - April 2015), and worked on
abstract machines for the geometry of synchronisation,
Yves Guiraud supervised the Master~2 internships of Pierre Giraud (M2 LMFI,
Univ.\ Paris~7, 2015), Amina Bendjaafar (M2 LMFI, Univ.\ Paris~7, 2016)
and Jean Vassalo (École Polytechnique, 2018), and a 6-month research
internship of Joey Beauvais-Feisthauer (L3 Univ.\ Ottowa, 2016).
Hugo Herbelin supervised the L3 internship of Meven Bertrand and the
pre-doctoral internship of Théo Zimmermann in 2016, as well as the
M2 internship of Charlotte Barot in 2017.
In 2015, Yann Régis-Gianas supervised the M2 internships of
Béatrice Carré and Jacques Pascal Deplaix, and the M1 internships
of Lélio Brun and of Loïc Runarvot. In 2016, he supervised the M1 internships of Paul Laforgue and Sylvain Ribstein, the L3 internship of Kostia Chardonnet, and the M2 internship of Colin Gonzalez. In 2018, he supervised
Loïc Peyrot (Master~1, Paris-7) about the development of a tool
to define exercises for the learn-ocaml platform in a single ML file;
Carine Morel (Master~1, Paris-7) about the development of a
user-friendly teaching-oriented documentation for the learn-ocaml
platform; Olivier Martinot (Licence~3, Paris 7) about the
implementation of a set of efficient incrementalised combinators for
list processing in cache-transfer style.
Alexis Saurin supervised Rémi Nollet (M2 LMFI, Paris-7, 2016, with Christine Tasson) on proof theory of
temporal logics and functional reactive programming type systems;
Ikram Cherigi (M2 LMFI, Paris-7, 2018, with Boban Velickovic)
about classical realisability and forcing in set theory;
Xavier Onfroy (M2 LMFI, Paris-7, 2018) on formalisation of
circular proofs in fixed-point logics and the decidability of
validity; Kostia Chardonnet (M1 MPRI, Paris-7, 2018) on
call-by-need calculus, degrees of lazyness and probabilistic $\lambda$-calculus.
Matthieu Sozeau supervised the M2 internships of Gabriel Lewertowsky
(with Nicolas Tabareau, MPRI, 2015) on ``Nominal Sets in Coq/SSReflect'',
Cyprien Mangin (MPRI, 2015) on ``Eliminating Dependent Pattern Matching
in Coq'' and Théo Winterhalter (MPRI, 2017) on ``Universes and
Reflection''.
%%%%%
\subsection{General audience actions}
% {\footnotesize\sl
% Mention other dissemination actions:
% general audience papers or talks, podcasts, interviews, videos, web sites, demos, etc. Length : max 1 page. TBR.}
Pierre-Louis Curien gave a talk in the Lycée Georges Dumézil (Vernon,
Eure, May 2018) on computer bugs and their prevention, on the occasion
of the 50th anniversary of this high school.
Hugo Herbelin wrote with Sandrine Blazy and Pierre Castéran in 2018 an
introduction to Coq for engineers edited by Techniques de
l'Ingénieur~\cite{blazy:hal-01645486}.
Pierre Letouzey and Yann Régis-Gianas took part in the ``Salon du jeu
mathématiques'' at Saint-Sulpice, Paris, in 2015.
Jean-Jacques Lévy is member of the Inria-Alumni's executive
committee (4 meetings in 2018) and organised the session about the
transparency of algorithms. He was invited by the French Academy of
Sciences to participate to the 2018 Hangzhou International Human
Resources Exchanges and Cooperation Conference (Hangzhou, November
2018). He gave a presentation about ``Science et Informatique'' at the
primary school le Coteau, Vaucresson (November 2018). He talked about
``L'informatique en 4 temps'' at the Alumni-UniThé seminar at Inria
Bordeaux (October 2018).
Yann Régis-Gianas co-organised the ``Journée Francilienne de
Programmation'', a programming contest between undergraduate students
of three universities of Paris (UPD, UPMC, UPS) in 2015, 2016, 2017
and 2018.
He organised the animation of the (computer science part of the) ``Fête de la Science'' event at the University Paris~7 in 2015 and 2016.
He gave
several presentations about ``What is programming?'' in primary and
high schools of Paris and its region during the whole period of
evaluation.
Since 2018, he is the project leader of the Learn-OCaml
project whose purpose is to support teaching the OCaml programming
language worldwide.
In collaboration with Roberto Di Cosmo and Ralf
Treinen, he has created a MOOC about the OCaml programming language (three editions, in 2015, 2016 and 2018).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Visibility}
% {\footnotesize\sl
% You could mention here your involvement in publishing activities,
% participation in the organisation of workshops/conferences,
% involvement and responsibilities in your scientific community. Length : max 2 page. TBR.}
%%%%%
\paragraph{Organisation of scientific events}
Pierre-Louis Curien organised a day of homage to the memory of
Maurice Nivat on February~6, 2018, at Univ. Paris~7.
Yves Guiraud organised, with Philippe Malbos (Univ.\ Lyon~1) and Samuel
Mimram (École Polytechnique), four editions of the Higher-Dimensional
Rewriting and Algebra (HDRA) workshop, in Warwaw (2015), Porto (2016)
and Oxford (2017, 2018).
He organised, with Dimitri Ara (Univ.\ Aix-Marseille) and
Samuel Mimram (École Polytechnique), the Categories in Homotopy and
Rewriting international conference, at the CIRM in Marseille (80
participants, 2017).
Yves Guiraud and Alexis Saurin, with Christine Tasson from IRIF,
organised the annual meeting of the Géocal and LAC working groups
of the GDR Informatique Mathématique (Paris, 2016).
Pierre Letouzey, Yann Régis-Gianas and Matthieu Sozeau organised the ``École de Printemps d'Informatique Théorique
2015'' in Fréjus about proof of programs.
Yann Régis-Gianas was multimedia chair of the organising committee of
POPL 2017, Paris.
Alexis Saurin organised and co-chaired with David Baelde the Paris
workshop in Oxford, UK, collocated with FLoC 2018.
Matthieu Sozeau co-organised and chaired the first Coq for Programming
Languages (CoqPL) workshop, collocated with POPL 2015 in Mumbai,
India.
Matthieu Sozeau co-organised with Nicolas Tabareau the 3rd Coq
Implementors Workshop in Le Croisic, France, in June 2017. It
included presentations from developers, both from France and abroad,
and a large amount of hacking.
Matthieu Sozeau co-organised and co-chaired with Nicolas Tabareau the
Coq Workshop 2018 in Oxford, UK, collocated with FLoC 2018.
%%%%%
\paragraph{Programme committees}
Pierre-Louis Curien is member of the programme committee of FSCD 2020.
Yves Guiraud was member of the programme committee of HDRA 2015, 2016,
2017 and 2018, and of IWC 2016.
Hugo Herbelin was member of the programme committees of the conference
FSCD 2017, of the TYPES 2017 venue, as well as of the PxTP 2017 and
CoqPL 2018 workshops, and of the conference POPL 2019.
Yann Régis-Gianas was member of the programme committee of JFLA 2018,
JFLA 2019, and PPDP 2018.
Alexis Saurin was member of the programme committee of the workshop
Coinduction in Type Theory (Chambéry, 2017), and of the workshop on Trends in Linear Logic and Applications (Oxford, 2017, satellite event of FSCD).
Matthieu Sozeau was member of the programme committees of FSCD 2016, ITP
2016 and CoqPL 2016, CoqPL 2017, ITP 2018 in Oxford during FLoC 2018,
and of the 13th Workshop on Logical and Semantic Frameworks with
Applications, Fortaleza, Brazil, 2018.
%%%%%
\paragraph{Steering committees}
Pierre-Louis Curien is member of the steering committee of the
international workshop Games for Logic and Programming Languages
(GaLoP), since 2006.
Pierre-Louis Curien and Hugo Herbelin were members of the steering
committee of the conference \emph{Typed Lambda Calculi and
Applications} (TLCA) until its merge with the conference \emph{Rewriting Techniques and Applications} in the new conference \emph{Formal Structures for Computation and Deduction} (FSCD), whose first
edition was held in Porto in 2016. Hugo Herbelin was a member of the
steering committee of FSCD until September 2017.
Hugo Herbelin is a member of the steering committee of the conference
TYPES since 2011.
Matthieu Sozeau is member of the steering committee of the Dependently
Typed Programming international workshop (DTP) since 2012.
%%%%%
\paragraph{Editorial boards}
Pierre-Louis Curien is editor in chief of the Cambridge Univ.
Press journal Mathematical Structures in Computer Science (since
January 2016).
Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau were co-editors of
the post-proceedings of the conference TYPES 2014, published in October 2015 as LIPICS volume 39.
Alexis Saurin is editing a special issue of MSCS dedicated to
contributions in honour of Dale Miller for his 60th birthday (almost completed at the date of this report).
%%%%%
\paragraph{Invited talks}
Pierre-Louis Curien gave invited talks at the GALOP 2015 (Games in
Logic and Programming) Workshop (London, 2015) on ``Sequential algorithms: old and new''; at the
``Journées Calculabilité 2016'' (GDR IM, Nice, 2016), on ``Comportement séquentiel et interactif des schémas de récursion primitive'';
at the annual meeting of the Géocal and LAC working groups of the GDR
Informatique Mathématique (Paris, 2016) on ''Opérades cycliques, arbres non enracinés et cohérence'';
at the annual meeting of the international ANR project Pace (between
Univ. of Bologna, ENS Lyon and Shanghai Jiaotong Univ.) on
``Cyclic Operads, Unrooted Trees, and Coherence''' (Shanghai, 2016); at the conference Categories for Homotopy Theory and
Rewriting on ``A syntactic approach to polynomial functors, polynomial
monads and opetopes'' (2017). He gave talks on the legacy of
Maurice Nivat at two special events organised to honour his memory:
special sessions in the Journées du GDR IM (École Polytechnique,
2018), and at ICALP 2018 (Prague, 2018).
Hugo Herbelin gave in 2016 an invited talk on ``Proving with side-effects'' at
the Days in Logic meeting in Lisbon, Portugal.
He gave an invited
talk on computing with Gôdel's completeness theorem using side effects
at the workshop Proof, Computation and Complexity in Bonn, 2018.
Jean-Jacques Lévy gave
an invited talk on ``Strongly connected components
in graphs, Formal proof of Tarjan 1972 algorithm'' at the LTP
(Langages, Types et Preuves) day, Saclay (2016). He gave a talk at the first Inria-CAS joint project VIP meeting, Paris (November 2018) on ``Comparing a formal proof in Why3, Coq and Isabelle''.
Yann Régis-Gianas gave an invited talk at the Conference for Trends in
Functional Programming in Education on the OCaml MOOC (2017).
He gave an invited talk about copatterns in OCaml at the ``Logique,
Types et Preuves'' workshop of the GDR GPL in 2018.
Alexis Saurin gave an invited talk, in the form of a distilled
tutorial, at WoC 2015, affiliated to ETAPS 2015 on ``Logical by
need''.
Matthieu Sozeau gave invited talks at the HoTT/UF workshop (Warsaw, 2016) on ``Coq support for Homotopy Type
Theory''; at the DeepSpec kickoff meeting
(Princeton, 2016), on ``Coq 8.6'' (together with
Maxime Dénès); at the International Conference on Mathematical
Software (Berlin, 2016), on ``Coq for HoTT''; at
the Categorical Logic and Univalent Foundations workshop (Leeds, UK,
2016), on ``Forcing Translations in Type Theory''; at the
Coq Workshop (Nancy, 2016), on ``Coq 8.6''. He gave an invited talk on ``The Predicative, Polymorphic,
Cumulative Calculus of Inductive Constructions'' at the TYPES 2018
International Conference on Types for Proofs and Programs in Braga,
Portugal, 2018. He gave an invited seminar entitled ``Programmer
en Coq'' at the Collège de France, on 2018, part of Xavier
Leroy's lectures on the Curry-Howard Isomorphism.
\paragraph{Research stays abroad}
Pierre-Louis Curien visited the Category Theory group at Macquarie Univ. for two months in 2016 (collaborative work on the combinatorial structure of type dependency). He
visited ECNU (Shanghai) for a month in 2017, and a month from in 2018 (collaborations with Yuxin Deng and Min Zhang) as invited professor.
He visited the Institute of Mathematics of the Serbian Academy of Sciences in Belgrade in 2018 for a week (collaboration with Zoran Petrić and other coauthors).
Jean-Jacques Lévy visited the Institute of Software of Chinese Academy of Sciences (ISCAS) in 2017 (project VIP and on-going work with Ran Chen) during two weeks. He gave talks at ISCAS hosted by Ying Jiang, and during a third week at ECNU Shanghai hosted by Min Zhang, USTC Suzhou (University of Science and Technology of China) hosted by Xinyu Feng, Nankai Univ. in Tianjin hosted by Chunfu Jia.
%As a part of his joint PhD, Étienne Miquey worked during two long periods in Montevideo within the Logic group of the Universidad de la República of Uruguay.
Hugo Herbelin participated to the Types, Sets and Constructions Trimester Program at the Hausdorff Research Institute of Mathematics in Bonn, in 2018.
%%%%%
\paragraph{Scientific expertise}
Pierre-Louis Curien has been member of the ``Comité de Sélection''
for a professor position in mathematics at Univ. Paris
7 in 2015. He has been member of the ``Comité de Sélection'' for a
professor position in discrete mathematics at Univ. Univ. Paul
Sabatier in Toulouse in 2016. He has been an expert for a hiring committee
for an assistant professor position in Logic, Computation and
Programming at Stockholm Univ. (2018).
Pierre-Louis Curien and Yves Guiraud have been members of the ``Comité
de sélection'' for an assistant professor position in mathematical
foundations of computer science at Univ. Paris~7 in 2017.
Yves Guiraud is a reviewer for the AMS MathReviews (since 2017). He
has been a reviewer for the Université Catholique de Louvain (2018).
Hugo Herbelin has been member of the ``Comité de Sélection'' for a
starting researcher position at INRIA Saclay in 2016. In 2018, he has
been a reviewer for FWF (Austrian research funding agency) and NKFI
(Hungarian research funding agency).
Hugo Herbelin and Yann Régis-Gianas have been members in 2016 of the
``Comité de Sélection'' for an assistant professor position at
CNAM in Paris.
Yann Régis-Gianas has been member of the ``Comité de Sélection''
for an assistant professor position at Univ. Paris Sud in
2016. He has been member of the ``Comité de Sélection'' for one
assistant professor position at IRIF in Paris in 2017 and for two
assistant professor positions at IRIF in Paris in 2018.
%%%%%
\paragraph{Research administration}
Pierre-Louis Curien is a member of the Scientific Council of the CIRM
(Centre International de Rencontres Mathématiques) (since 2013).
Pierre-Louis Curien, Yves Guiraud and Hugo Herbelin are members of the
scientific council of the Computer Science department of Univ.
Paris~7 (since January 2016).
Yves Guiraud is the head of the ``Preuves, Programmes et Systèmes''
(PPS) pole of the IRIF laboratory (since April 2016), and a member of
the IRIF direction council (since September 2017). He was a member of
the IRIF laboratory council (January 2016 - December 2017), and the
developer and maintainer of the new IRIF website (September 2015 -
December 2018).
Hugo Herbelin is the head of the ``Preuves et Programmes'' thematic
team of IRIF (since September 2017).
Since 2018, Yann Régis-Gianas is a member of the Executive Committee of the OCaml
Foundation, acting as a representative of the teaching community.
Since 2018, in collaboration with Emmanuel Chailloux (UPMC), he is
organising the next four years of IRILL, an initiative about
innovation in free software.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Funding}
\label{finance}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{National initiatives}
% {\footnotesize\sl Give a short description (5 lines) for each national initiative (ANR, PIA, \ldots), including its name, the list of research groups involved, and the total amount of the grant. TBR.}
Pierre-Louis Curien (coordinator) and Yves Guiraud (local coordinator) have been members of the three-year
Focal project of the IDEX Sorbonne Paris Cité (July 2013 to June
2016). This project concerned the interactions between
higher rewriting and combinatorial and higher algebra, and was joint
with Univ.\ Paris~13. It funded the PhD
grant of Cyrille Chenavier.
Pierre-Louis Curien (coordinator) and Yves Guiraud (local coordinator) have been members of the four-year Cathre
ANR project (January 2014 to December 2017). This project investigated
the general theory of higher categories, the development of
a library of rewriting methods for algebra, and
applications in the fields of combinatorial linear algebra,
combinatorial group theory and theoretical computer science. This
project was joint with Univ.\ Paris~13, École Polytechnique, Univ.\ Lyon~1, Univ.\ Saint-Étienne), Univ.\ Aix-Marseille and Univ.\ Toulouse~3. It funded the PhD grant of Maxime Lucas.
Pierre-Louis Curien, Yves Guiraud, Hugo Herbelin and Alexis Saurin are
members of the GDR Informatique Mathématique, in the
LHC (Logique, homotopie, catégories) and Scalp (Structures formelles pour le calcul et les preuves) working groups. Alexis Saurin is the coordinator of the Scalp working group.
Pierre-Louis Curien, Yves Guiraud (local coordinator) and Matthieu
Sozeau are members of the GDR Topologie Algébrique, federating French
researchers working on classical topics of algebraic topology and
homological algebra, such as homotopy theory, group homology,
K-theory, deformation theory, and on more recent interactions of
topology with other themes, such as higher categories and theoretical
computer science.
Yves Guiraud is member of the GDR Tresses, federating French
researchers working on algebraic, algorithmic and topological aspects
of braid groups, low-dimensional topology, and connected subjects.
Hugo Herbelin was the coordinator of the PPS site of the ANR project Récré
(January 2012 to mid 2016), about realisability and rewriting, with
applications to proving with side-effects and concurrency.
Hugo Herbelin, Matthieu Sozeau
and Yann Régis-Gianas have been members of the ANR project Paral-ITP (November
2011 to June 2015), aimed at preparing the Coq and Isabelle interactive
theorem provers to a new generation of user interfaces thanks to
massive parallelism and incremental type-checking.
Since 2014, Yann Régis-Gianas collaborates with Mitsubishi Rennes on
the topic of differential semantics; this collaboration led to the
CIFRE grant for the PhD of Thibaut Girka. Since 2018, he collaborates with ANSSI on the topic of certified ful
programming in Coq. Since 2016, he is a member of the
ANR project COLIS dedicated to the verification of Linux distribution
installation scripts. This project is joint with Univ.\ Paris-Sud and Univ.\ Lille.
Yann Régis-Gianas and Alexis Saurin (coordinator) are members of the
four-year ANR project RAPIDO (started in January 2015),
investigating the use of proof-theoretical methods to reason and
program on infinite data objects. The goal of the project is to
develop logical systems capturing infinite proofs (proof systems with
least and greatest fixpoints as well as infinitary proof systems), to
design and study programming languages for manipulating infinite
data, such as streams, both from a syntactical and semantical point of
view. This project is joint with ENS Cachan and ENS Lyon.
%Matthieu Sozeau has been member of the ANR Typex (Types and
%certification for XML) and was coordinator of one of the tasks of
%the project on formalisation and certification of XML tools.
%The project kicked-off in January 2012 and was a joint
%project with LRI, PPS and INRIA Grenoble. \yves{hors période}
Matthieu Sozeau is a member of the CoqHoTT ERC project (2015-2020) led
by Nicolas Tabareau (Gallinette team, Inria Nantes).
The PhD grant of Antoine Allioux, the post-doctoral grant of Eric Finster,
and Amin Timany's two-month visit are funded by the CoqHoTT ERC.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{European projects}
% {\footnotesize\sl Give a short description (5 lines) for each European project, including the type of project (ERC, H2020, \ldots), its name, the list of partners, and the total amount of the grant. TBR.}
Hugo Herbelin is a deputy representative of France in the COST action EUTYPES (European research network on types for programming and verification, 2016-2020, led by Herman Geuvers, Univ.\ Nijmegen). This action aims at
promoting: (1) the synergy between theoretical computer scientists, logicians and mathematicians to develop new foundations for type theory, for example as based on the recent development of homotopy type theory; (2) the joint development of type-theoretic tools like proof assistants and integrated programming environments; (3) the study of dependent types for programming and its deployment in software development; (4) the study of dependent types for verification and its deployment in software analysis and verification.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Industrial contracts}
% {\footnotesize\sl Give a short description (5 lines) for each contract including the name of the company, the object of the collaboration, and the total amount of the grant. TBR.}
Since 2014, Yann Régis-Gianas collaborates with MERCE (Mitsubishi
Electrics Research and Development, located in Rennes) on the
topic of the certification of software evolutions. This contract
funded a PhD grant.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Inria Project Labs, Exploratory Research Actions and Technological Development Actions}
% {\footnotesize\sl Give a short description (5 lines) for each IPL, PRE, and ADT including its name and a list of research groups involved. TBR.}
The Coq development was supported by the ADT Coq (ADT-108) during the
evaluation period, which helped recruit an engineer, Matej Košic, in
2015-2016 in the team who then moved to Marelle for another year. He
focused on continuous integration and packaging. In 2017 and 2018, the
DGD-T gave 15k euros of funding (9k for Marelle, 6k for $\pi r^2$) and
24k shared among Gallinette, $\pi r^2$ and Marelle. This funding helps with
dissemination missions and the organisation of developer and researcher
workshops (traditionally attached to POPL and ITP), and working groups,
which have since moved to a more decentralised setup through
video-conferencing.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Associated teams and other international projects}
% {\footnotesize\sl Give a short description (5 lines) for each associated team/project, including the type of project, its name and the list of partners. TBR.}
Pierre-Louis Curien is a member of the CRECOGI associate team (2015-2018, renewed in 2018), coordinated by Ugo Dal Lago (team FoCUS, Inria Sophia and Bologna) and by Ichiro Hasuo (NII, Tokyo).
Presentation of CRECOGI (Concurrent, Resourceful and full Computation, by Geometry of Interaction): Game semantics and geometry of interaction (GoI) are two closely related frameworks whose strength is to have the characters of both a denotational and an operational semantics.
This project aims at investigating the application of GoI to concurrent, resourceful, and effectful computation, thus paving the way to the deployment of GoI-based correct-by-construction compilers in real-world software developments in fields like (massively parallel) high-performance computing, embedded and cyberphysical systems, and big data.
Pierre-Louis Curien is principal investigator on the French side for the Inria - Chinese Academy of Sciences project ``Verification, Interaction, and Proofs''. The principal investigator on the Chinese side is Ying Jiang, from the Institute of Software in Beijing. The participants of the project on the French side are Pierre-Louis Curien and Jean-Jacques Lévy, as well as other members of IRIF,
and Gilles Dowek (Deducteam team).
The project funded the postdoc of Kailiang Ji at IRIF (December 2017 to March 2019).
Presentation of VIP:
The aim of this project is to bring specialists of model-checking and proof-checking together
(the ``V'' and the ``P'' of the acronym). Applications in the realm of distributed computation, or concurrency theory (the ``I'') are particularly targeted.
Pierre-Louis Curien and Tarmo Uustalu (Tallin Univ. of Technology and Univ. of Reykjavik) are the principal investigators of the bilateral Parrott project (Partenariat Hubert Curien) ``Mathematical structures for dualities in programming languages'' (2017 and 2018).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Other funding}
% {\footnotesize\sl Give a short description (5 lines) for each other funding source. TBR.}
Pierre-Louis Curien participated to the ANR International French-Chinese project LOCALI (Logical Approach to Novel Computational Paradigms), coordinated by Gilles Dowek (Project-team Deducteam). This project ended in July 2017.
Matthieu Sozeau is part of an international collaboration network CSEC ``Certified Software Engineering in Coq'' funded by Inria Chile, Conicyt and the CoqHoTT ERC, which officially started in early 2018. The participants include Eric Tanter (primary investigator) and Nicolas Tabareau.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Follow up to the previous evaluation}
% {\footnotesize\sl Describe how the main comments/suggestions/etc. made in the last evaluation by the evaluators, the Comité des projets and the Commission d'Évaluation (if any) have been taken into account during the evaluation period. In case you encountered difficulties to address some of the comments explain why. Length: min 1 page, max 2 pages. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
We answer to comments and suggestions from the 2015 evaluation report of the team.
%%%%%
\paragraph{Principal strengths and weaknesses of the project (pp.~35-36)}
\begin{itemize}
\item \emph{``Despite the stated interest in dependently-typed programming languages, the emphasis of the project seems to be on the proof theory side.''}
There was a strong focus during the evaluation period on certified
programming with dependent types across the team. We lifted
proof-theory results to the dependent case (lazy dependent choice), we
studied programming with effects in dependent type theory (Guillaume
Claret's PhD, Yann Régis-Gianas' collaboration with ANSSI), and we
enhanced the treatment of dependent pattern-matching and recursion
(Boutillier's thesis, the \Equations package) and of how to deal with
proof-irrelevance. Finally we collaborate on efficient compilation of
dependently-typed programs in the setting of the CertiCoq project.
\item \emph{``The project can increase its impact by further strengthening the connections among the subgroups within the team. For example, avenues for cross-fertilisation between higher-dimensional rewriting and homotopy type theory should be investigated.''}
We agree that there are similarities between the two research fields,
such as polygraphic resolutions vs.\ higher inductive types, or
weak representations vs.\ dependent types, but formal dictionaries have proved to be quite hard to build. As a first step to understand how to relate these two worlds, a postdoc was funded for 2017-2019, and a PhD was started in 2018 with the objective to better understand how to formalise basic algebraic structures in homotopy type theory.
\item \emph{``In a similar vein, more could be done to transfer advances in the metatheory of Coq to the design and implementation of the proof assistant; a possible example is certified extraction.''}
The MetaCoq project aims to do just that: providing a rigorous,
mechanised model of the evolving type theory and linking it to a
reference implementation. This is used as a target theory, to extend
Coq through verified translations, which is a focus of the CoqHoTT
project. It is also the source of an extraction procedure that is
already used in the CertiCoq compiler; its correctness proof is
ongoing work.
\item \emph{``Finally industrial interaction and partnership, which appears sporadic [\dots], could be developed more systematically''.}
We have solid contacts with Mitsubishi and Tweag~I/O. We are open to
collaborations which would emerge naturally. We indirectly support
industrial use of Coq as part of our collaboration with ANSSI which is
in charge of validating industrial applications certified in Coq. Of
course, more industrial interactions in the context of Coq can go
through a structure like the Coq consortium.
\end{itemize}
%%%%%
\paragraph{Plan for the next period (pp.~36-37)}
\begin{itemize}
\item \emph{``A natural and relevant direction concerns algebraic effects in the sense of Plotkin, Power and Hyland, and developed by Melliès, Staton and others. We would suggest that this topic be added to the research plan.''}
We were not familiar enough with algebraic effects to add it
explicitly to our research plan. We are focusing on effects where
logic and programming meet and it is not clear what algebraic effects
could mean in the context of logic. Nevertheless we stay informed
about this topic. For instance, Hugo Herbelin has been a reviewer of
the PhD of Jirka Maršík on algebraic effects.
\item \emph{``A new objective of the plan, Reasoning and programming with infinite data, is in line with the team's general goal of finding logical explications of computational phenomena [\dots]. We would encourage interactions with research groups elsewhere working on the same theme.''}
Several connections were made:
first, the ANR project RAPIDO helped building strong relations with researchers at LSV and LIP over the whole evaluation period; second, various connections were made, most notably with groups in the UK, Sweden, Denmark, Italy and Japan; last, through the organisation of a workshop in July 2018, additional interactions were created (A. Saurin is involved in a follow up workshop taking place in Sweden late 2019).
\end{itemize}
%%%%%
\paragraph{Opportunities and risks/difficulties faced by the project (p.~37)}
\begin{itemize}
\item \emph{``We recommend that the interface between developers and users [of Coq] be improved with the appropriate engineering support.''}
Inria has been of great help improving engineering support: two
engineers are now working full-time on Coq development and have
growing expertise on the system, interacting with both researchers
developing the system and users. The last four years have seen an
increase of interactions between users and developers, through public
communication channels, continued animation of workshops and the
introduction of ``coding sprints'', an open package index and the
coq-community effort. We believe that the interface has greatly
improved in that time frame, even if much remains to do.
\item \emph{``We sensed the willingness of the relatively small group of researchers working on these topics [(effective higher algebra)] to engage and establish links with the rest of the team; we would strongly encourage such interactions.''}
See above (second item of ``Principal strengths and weaknesses of the project'').
\item \emph{``Finally as the scientific leader approaches retirement, there is an urgent need for succession planning and the grooming of potential leaders.''}
The current scientific leader will retire in October~2019. Considering that the team is ten years old, the members will propose a new scientific project in a close future, in agreement with the direction of the INRIA Paris center.
\end{itemize}
%%%%%
\paragraph{Recommended actions and suggested measures of success (p.~38)}
\begin{itemize}
\item \emph{``To address the shortage of qualified engineers, we recommend that INRIA establish longer fixed-term (4 or 5 years) advanced engineer positions linked to software development. During the recruitment process, the applicants should be evaluated as software engineers, not academic researchers.''}
This wish has been granted by Inria, which is now employing two
full-time engineers with PhDs in the field (Maxime Dénès in Nice and
Vincent Laporte in Rennes), as part of the Coq
consortium. The hope is to be able to secure external funding from
academic and industrial partners in the future, as the development of
Coq benefits to a community far larger than Inria. Also, we note that
the new INRIA CEO considers the possibility for a few research teams with heavy development duties to host a full-time research engineer. We are obviously particularly interested by such an opportunity.
\item \emph{``Seriously consider moving to a github-like model in which external 'pull requests' are actively encouraged and accepted, particularly in areas outside of the proof-critical kernel. INRIA should also seriously consider anything that could further facilitate community involvement, for example the integration of issue tracking with source control.''}
The entire development has moved to the github platform and external
contributions are encouraged and welcomed (to wit, the last versions
had about 50 contributors from all around the world). The development
team actively uses source control, discussions and reviews of
pull-requests, issue tracking and continuous integration. The move of
the bugtracker from BugZilla to Github was performed by Théo Zimmermann
and resulted in a useful empirical software engineering study.
\item \emph{``Encourage design input from programming language and
compiler experts, not just members of the $\pi r^2$ team. Much of the
Coq system lives above the level of the kernel type theory. Teams
Marelle and Gallium, and external experts, could have a role
here.''}
Examples of such design input appear more often today. The
collaboration with the CertiCoq team led by Andrew Appel is such an
example, and motivates for example a change of representation of the
pattern-matching construct that Hugo Herbelin is implementing in the
kernel. The design of the new proof-irrelevance system was done in
collaboration with members of the Gallinette team and a member of the
Agda development team. In general, the Coq development team is made of
engineers and researchers at Inria and elsewhere who collaborate on
the design of all components of the tool, some of which $\pi r^2$ has
little expertise on, such as user interfaces.
At the level of the ecosystem, Coq's new package manager is based on
OCaml's (thanks to work by Guillaume Claret) and the new
coq-community effort launched by Théo Zimmermann both draws from the
elm-community initiative and inspires the ocaml-community effort.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Objectives for the next four years}
% {\footnotesize\sl Indicate the main research directions and their scientific and application objectives, open problems to be solved, anticipated risks and the means (staff requirement) to achieve those objectives. Length: min 1 page, max 2 pages. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The project-team will end soon, as its leader retires in late 2019. The discussion on a new scientific project has started and will be resumed after the writing of this evaluation report. Here, we list the research objectives that we have already identified in the continuity of the scientific programme of~$\pi r^2$, including some items that emphasise convergences between the present axes of research.
% \paragraph{The convergence between proofs, programs, topological spaces, algebra}
% The Curry-Howard correspondence and its extensions connect proofs to
% programs, and proposition to types. This led in particular to the
% design of type theory, which is both a logical system and a
% programming language. The Lambek correspondence and its extension
% additionally connects category theory to logic and computer
% science. The space-as-type correspondence additionally connects types
% to topological spaces up to homotopy. In particular, it shows that
% equality proofs in logic, and in particular in type theory, share the
% same structure as paths in spaces. Higher-dimensional categories are
% themselves algebraic models of spaces up to homotopy, tying the loop
% with type theory. Programming languages support side effects, which
% in turn connect to logical translations such as the forcing
% translation. Side effects are interpreted categorically as monads and
% comonads.
% Beyond the use of different syntaxes and different vocabularies, and
% besides the difference of focus, it starts to be clear that an
% irreversible move towards the formal convergence of the mathematical
% structures studied by these fields is ongoing.
% In the next years, in the context of this convergence, we plan, in
% addition to complete important ongoing works (in particular the
% ability to prove with side effects), to further investigate the
% following directions:
%%%%%
\paragraph{Proof theory and the Curry-Howard correspondence}
\begin{itemize}
\item \emph{Effects in logic}. We intend to pursue and disseminate our
results on proving with side effects, connecting forcing and memory
assignment. We aim at a unifying framework characterising
programming effects and their semantics, as well as logical
translations and their underlying computational contents, addressing
also the case of realisability.
\item \emph{Axiom of choice}. We intend to investigate further the
computational contents of different variants of the axiom of choice,
including the classical extensional axiom of choice, last missing
piece not entering the proof-as-program correspondence yet.
\item \emph{A computational approach to reverse mathematics}. Reverse
mathematics relate theorems of similar logical strength, but, from a
proof-as-program point of view, reverse mathematics results can also
be seen as transformations of programs, which we shall investigate.
\end{itemize}
%%%%%
\paragraph{Homotopy type theory}
\begin{itemize}
\item \emph{Cubical type theory}. Cubical type theory is an
alternative approach to the characterisation of (higher-dimensional)
equality in type theory. We intend to investigate its properties and
the connections with iterated realisability. As a prospective
direction, we plan to analyse the structure of higher-dimensional
equality proofs as computational data.
\item \emph{Formalisation of algebraic structures}. Around the PhD
thesis of Antoine Allioux, the similarities of higher algebra and
homotopy type theory will continue to be investigated: in particular,
the potential connexions between polygraphic resolutions and higher
inductive types, and also between weak higher representations (i.e.\
pseudofunctors with values into higher categories) and dependent types.
\end{itemize}
%%%%%
\paragraph{Certified programming}
\begin{itemize}
\item \emph{Coq as a state-of-the art dependently-typed programming
language}. Coq's functional programming language provides primitives
to express a wide variety of programs, however we are in need of
higher-level tools to make programming and proving with dependent
types more accessible in the system. Building on our expertise on
compilation of pattern-matching, co-patterns and (co-)recursion, we
plan to provide more robust, flexible and expressive tools for the
definition of programs and their proofs. This work goes hand-in-hand
with continued foundational advances in the core theory: we will
investigate the use of definitional proof-irrelevance to ease
programming with refinement types and the introduction of
inductive-inductive and inductive-recursive types in the core type
theory in particular.
\item \emph{Coq as a general purpose programming language}. Effectful
programming in Coq is possible~\cite{letan:hal-01799712}: not only can we
modularly define programs that interact with their environment,
but we know how to reason about these programs inside Coq. The
question is now to scale up these techniques to turn Coq into a
realistic programming language, following the same path as the
Haskell programming language took in the 1990s. To achieve this
project, we need to develop a proper compilation chain for Coq
programs and a well-suited \emph{Foreign Function Interface} to be
able to call system primitives and external libraries. Once this
will be done, an important and difficult work will be the design of
a standard library (file manipulation, networking, OS interaction)
with rich specifications.
\item \emph{Gallina as a meta-programming language for Coq}.
Today, Coq is made of three languages: Gallina for specifications
and programming, Ltac for proof scripting and Vernacular for
meta-level definitions. This multiplication of languages increases
the heterogeneity of the system interface, it creates unnecessary
learning difficulties, and it leads to redundancy in the code base.
%
The Mtac2 project is demonstrating that Gallina is a good replacement to Ltac:
it provides a typed language with clear semantics which significantly
improves the quality of proof scripts. Besides, the clear specification of Mtac2
allowed us to start the implementation of a JIT compiler for Mtac2
(reusing a machinery for native computation already present in Coq). That
project was out of reach if applied to Ltac.
%
Continuing in that direction, the next step is to replace Vernacular
by Gallina. This project is ambitious because Vernacular has a large
range of mechanisms (small-scale and large-scale definitions
management, notations, etc.), but if we can control these mechanisms
programmatically from Gallina itself, it would be possible to
naturally write generative programs, which are encoded using
typeclass instances today.
\item \emph{Certifiying Coq}. In another direction, using the deep
embedding of Coq in Coq provided by the MetaCoq project, we can hope
to (partially) verify the implementation of Coq itself inside Coq and
provide a mechanised specification of its theory. On top of that, it
will be possible to study and verify extensions of that theory
(i.e.\ through translations from higher-level type theories or DSLs)
and the extraction and compilation phases from Coq terms
themselves. We plan to complete these projects, providing a
fully-certified program development chain from high-level
dependently-typed programs down to machine code.
\item \emph{A certification framework for differential functional programs}.
Even though cache-transfer-style static differentiation provides a
way to compose incremental programs in a higher-order setting, the
incremental version of base operations (over lists, trees, etc.)
still has to be implemented. Manual incrementalisation of programs
is error-prone and difficult because
%
(i) if a data type has~$n$ constructors and~$m$ kinds of change,
writing an incremental program requires~$nm$ cases;
%
(ii) change application is often undefined (think about
removing an element from an empty list) and this leads to many limit
cases in incrementalised programs and to complex preconditions;
%
(iii) incrementalised higher-order combinators, typically iterators,
can exploit the properties of their input functions to compute their
own differential more efficiency;
%
(iv) to be efficient, incremental programs use complex data
structures.
Coq is a programming language of choice to deal with these problems,
because it allows program-proof co-design leading to programs which
are correct by construction. We have started the development of a
standard library of certified incrementalised primitives named
$\Delta$Coq as well as a tool named $\Delta$Caml which allows an
OCaml program to automatically integrate these primitives in larger
incrementalised programs.
\end{itemize}
%%%%%
\paragraph{Reasoning and programming with infinite data}
\begin{itemize}
\item \emph{Pursuing the investigation of circular proofs}. We aim at developing more expressive validity conditions and more flexible proof systems for infinite and circular proofs (bouncing threads in proof nets and natural deduction systems), and at developing denotational semantics of non-wellfounded proofs of $\mu$MALL.
\item \emph{Investigating applications of circular proofs to programming}.
We wish to undertake a formal study of the relationships between various ways to validate/ensure productivity of (co)inductive computation/validity of (co)inductive reasoning: thread-based in connection with non-wellfounded proofs, size-change principle in connection with program termination, modality based in connection with synchronous programming.
%
We also want to investigate whether circular proofs and thread-based validity can offer interesting alternatives to guard condition for Coq's coinductve types.
\item \emph{Applications of circular proofs}. We plan to investigate in the near future the use of circular proofs in modelling the introduction of (co)inductive types in quantum programming. This is a joint project with Benoît Valiron (Centrale Supélec): a previous work by Valiron considers a language of reversible patterns (as a core system for quantum programming), which can be viewed as MALL isos in a language where MALL is extended with an inductive type of lists. Non-overlapping and completeness of patterns is achieved in a system reminiscent of circular focusing proofs, and we plan to extend this language with generic (co)inductive type constructions and relate precisely $\mu$MALL focusing with the above mentioned type derivations on patterns.
\end{itemize}
%%%%%
\paragraph{Effective algebra}
\begin{itemize}
\item \emph{Generalised polygraphs}. Notions of polygraphs are now well known for structures such as monoids, categories or associative algebras, which have the common property to be monoids is specific monoidal categories. We plan to extend the definition of polygraph to the whole class of monoids in monoidal categories, also including operads, Lawvere theories, higher-order theories (including $\lambda$-calculus and type theory), etc. This will pave the way to new rewriting methods to compute on these objects (collaboration with Marcelo Fiore, Univ.\ Cambridge).
\item \emph{Garside methods in rewriting}. Originating in the study of braid groups, Garside theory provides alternative ways of computing normal forms and resolutions for monoids~\footcite{DehornoyDigneGodelleKrammerMichel13}. Building on~\cite{dehornoy:hal-01141226}, we will continue the integration of Garside methods into rewriting theory, with a view towards an improved completion procedure that can also add new generators to a given presentation (collaboration with Matthieu Picantin, Univ.\ Paris~7).
\item \emph{New applications in effective algebra}. The new, Garside-improved rewriting methods will be applied to obtain better results and new constructions in effective algebra. The main objective is to compute new resolutions for specific monoids, based on Garside families, leading to smaller results than the known rewriting methods (collaboration with Matthieu Picantin, Univ.\ Paris~7); this would generalise the results of~\cite{gaussent:hal-00682233} and potentially lead to new progress around the so-called $K(\pi,1)$ conjecture, that is deeply linked to the computation of certain precise polygraphic resolutions of Artin groups (planned collaboration with Stéphane Gaussent, Univ.\ Saint-Étienne, and Philippe Malbos, Univ.\ Lyon~1). Also, the new completion procedure should explain the normal forms obtained in~\footcite{AmyChenRoss18} for quantum circuits on the CNOT and~T gates, and possibly provide normal forms for other sets of gates (planned collaboration with Julien Ross, Univ.\ Dalhousie).
\end{itemize}
%\yves{Chapeau présentant la vision et les 4 axes...}
%
%\yves{Pour chaque axe, on peut déjà faire une liste des travaux en cours}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Development of Coq}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Quelques phrases...
%
%\begin{itemize}
%\item Maintenance quotidienne
%\item Langages de tactiques
%\item \dots
%\item Langages diagrammatiques et interfaces ?
%\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Proof theory and type theory}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Quelques phrases...
%\begin{itemize}
%\item Fondations logiques
%\item Correspondance de Curry-Howard (extensions)
%\item Théorie homotopique des types
%\item Théorie des types cubiques?
% Better syntaxes for higher inductive types and links to parametricity.
% Hugo Herbelin worked on a syntax for a variant of Cohen, Coquand,
% Huber and Mörtberg's Cubical Type Theory where equality on types is
% defined to be equivalence of types, thus satisfying univalence by
% constructions.
%\item \dots
%\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Certification of programs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Quelques phrases...
%
%\begin{itemize}
%\item Extraction de programmes
%\item Preuves de programmes
%\item Langages de programmation certifiés
%\item \dots
%\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Mechanisation of algebra}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Quelques phrases...
%
%\begin{itemize}
%\item Formalisation des structures algébriques : aspects théoriques (opérades, théories de Lawvere, algèbre universelle en général) et pratiques (résolutions polygraphiques et HITs, représentations faibles et éliminateurs de types)
%\item Calcul algébrique mécanisé : réécriture, théorie de Garside -> KGB et nouvelles formes normales, amélioration du calcul de résolutions polygraphiques
%\item Applications en algèbre : cohérence, algèbre homotopique, théorie des représentations, etc.
%\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newpage
\section{Bibliography of the project-team}
%{\footnotesize\sl Limited to the evaluation period. See below for references to older publications by the team or to publications by others. The \verb|Export_RA.bib| file is to be generated from HAL using \verb|haltools.inria.fr|. TBR.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{small}
\nocite{*}
\bibliographystyle{bibevalurl}
\bibliography{Export_RA}
\end{small}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newpage
\section{Other citations}
%{\footnotesize\sl This is the additional bibliography for references other than publications by the team during the evaluation period. Put them in file \verb|footbib.bib| and use \verb|\footcite| instead of \verb|\cite| to reference. Length: max 1 page. TBR.}
\let\thebibliography=\oldthebibliography
\let\thebibliographyend=\oldthebibliographyend
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{small}
\bibliographystyleref{alpha}
\bibliographyref{footbib}
\end{small}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%