<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\documentclass[a4paper,11pt]{article}

% Document tirÃ© de https://www.monperrus.net/martin/template-latex-anr,
% adaptÃ© Ã&nbsp; l'AAP 2019 JCJC
% en particulier de la trame LibreOffice proposÃ©e:
%   http://www.agence-nationale-recherche.fr/fileadmin/aap/2019/aapg-anr-2019-pre-proposition.docx

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
%% Sans-serif Arial-like fonts
\renewcommand{\rmdefault}{phv}
\renewcommand{\sfdefault}{phv}
\usepackage{tabularx}
\usepackage{graphicx}
\usepackage{eurosym}
\usepackage{xspace}
\usepackage[colorlinks,linkcolor=blue,citecolor=blue,urlcolor=magenta]{hyperref}
\setlength{\footskip}{2cm}
\setlength{\headheight}{2cm}
\usepackage[lmargin=2cm,rmargin=2cm,tmargin=3.5cm,bmargin=1cm,includefoot]{geometry}
\usepackage{lastpage}%% to get the total number of pages

\usepackage{pdflscape}

\usepackage{datetime}

\newcommand{\projectname}[0]{\textsc{Repro}\xspace}
\newcommand{\projectduration}[0]{4 years}
\newcommand{\projectcost}[0]{\EUR{227,000}}
\newcommand{\coordinator}{Gabriel Scherer}
\newcommand{\selectioncommittee}%
  {CES 48 - Fondements du numÃ©rique : informatique, automatique, traitement du signal}

\usepackage{amsmath}
\usepackage{amssymb}

% more compact paragraph style
\renewcommand{\paragraph}[1]{\vspace{\baselineskip}\textbf{#1}.}

\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\setlength{\headheight}{80pt}
\fancyhead[C]{\includegraphics[height=1cm]{anr-logo/ANR-logo.pdf}
\hfill
\projectname{}
\hfill
Programme JCJC
\\AAPG-ANR-2019
\hfill
CordonnÃ© par: \coordinator
\hfill
\projectduration, \projectcost
\\
\selectioncommittee
}
\cfoot{\thepage}

\newcommand{\content}[1]{\emph{#1}\\}

\usepackage{natbib}
\setlength{\bibsep}{0.0pt}
\bibliographystyle{abbrvnat}
\citestyle{authoryear}

% http://nw360.blogspot.com/2007/12/rename-bibliography-title-in-latex.html
\renewcommand\refname{\vspace{-1cm}}

%\usepackage{xcomment}
\newenvironment{xcomment}{\em}{}

\begin{document}

\begin{center}
%  \textbf{DRAFT} Last update at \currenttime, \today\\
  {\huge
    \projectname{}: Searching for\\ Canonical \textbf{Re}presentations of \textbf{Pro}grams}\\[1em]
  % Chercher les reprÃ©sentations canoniques des programmes

  {\large
    Principal Investigator (PI): \coordinator, \emph{ChargÃ© de recherche} at INRIA
  }
\end{center}

% \begin{xcomment}
%   Utilisez une mise en page permettant une lecture confortable du
%   document (page A4, calibri 11 ou Ã©quivalent, interligne simple,
%   marges 2 cm ou plus, numÃ©rotation des pages).

%   Le site de soumission refuse le tÃ©lÃ©chargement dâ€™un document de plus
%   de 4 pages ou dans un format autre que pdf. Aucune annexe nâ€™est
%   acceptÃ©e. Les CV du coordinateur et des responsables scientifiques
%   des Ã©ventuels partenaires sont Ã&nbsp; complÃ©ter en ligne sur le site de
%   soumission.

%   La rÃ©daction de votre prÃ©-proposition doit permettre son Ã©valuation
%   selon les 2 critÃ¨res dâ€™Ã©valuation dÃ©finis dans le texte de lâ€™appel
%   Ã&nbsp; projets gÃ©nÃ©rique 2019Â&nbsp;: Â«Â&nbsp;QualitÃ© et ambition scientifiqueÂ&nbsp;Â» et
%   Â«Â&nbsp;Organisation et rÃ©alisation du projetÂ&nbsp;Â». Il est nÃ©cessaire de se
%   reporter au texte afin dâ€™en connaitre les sous-critÃ¨res,
%   diffÃ©renciÃ©s selon lâ€™instrument de financement choisi.
% \end{xcomment}

\vspace{-2em}
\section{Scientific context, positioning and objectives}
% Pre-proposalâ€™s context, positioning and objective(s)

The \projectname{} project aims to
\begin{enumerate}
\vspace{-.6em}
\item deepen our understanding of the structure of computer programs
  by discovering \emph{canonical representations} for fundamental
  programming languages, and to
\vspace{-.6em}
\item explore the application of canonical representations to the
  problems of \emph{program equivalence checking} and \emph{program
    synthesis}.
\end{enumerate}

Arithmetic (sum and product) expressions in one variable $x$, such as
$(1 + 2 * x) * (1 + x)$, \emph{represent} a certain category of
functions from real numbers to real numbers. This representation
admits redundancies, in the sense that distinct expressions, such as
$(a + b) * x$ and $a * x + b * x$, may represent the same function. On
the other hand, \emph{polynomials}, which can be described formally as
either $0$ or a non-empty sum of the form
$\sum_{0 \leqslant k \leqslant d} c_k x^k$ with $c_d &lt;&gt; 0$, are
a canonical representation of product/sum functions in one variable:
if two polynomials have distinct coefficients, they represent distinct
functions.

A canonical representation has more structure: its definition encodes
more of the meaning of the objects being represented. For example, it
is non-obvious whether an arithmetic expression is constant (for all
values of $x$), while this question can be easily decided for
polynomials: it is constant when it is $0$ or its degree is $0$. In
general, polynomials are much more convenient to manipulate for
virtually any application. They are the ubiquitous choice of
representation when studying these objects.

Little is known about the canonical representation of computer
programs. Representing programs by their source code admits many
redundancies: the sources may be different in inessential ways
(choice of variables, order of computations, but also important
changes in program structure for example), which make no observable
difference in the behavior of the executing program.

Program equivalence has been studied for formal, idealized programming
languages known as $\lambda$-calculi. It strongly depends on the forms
of computations available in the programming language studied, in
particular the datastructures it can manipulate. In presence of only
functions and finite products (pairs of values), canonical
representations (called $\beta\eta$-normal forms) are
known~\citep*{boehm1968%,statman1983
}. But adding finite sums (disjoint union datatypes, in
particular booleans) gives a richer notion of program
equivalence. Non-empty sums have been studied since the
nineties~\citep*{ghani1995%,dougherty2000,altenkirch2001,fiore2006,lindley2007
}, providing partial proposals for canonical forms, and the case of
general finite sums (including empty sums) was proposed as an
important open problem to the programming language community in 1995.

In the 2010s, several groups~\citep*{ahmad2010,scherer2015,Ilik2017}
simultaneously developed the idea of using ideas of \emph{proof
  theory}, which had made progress on the quest for canonical
representations of proofs. A notion of particular interest is
\emph{focusing}, a discipline to reduce non-determinism during proof
search by imposing more structure on proofs, providing canonical
representations in some logics~\citep*{%focusing-andreoli,
multifocus}. By the Curry-Howard isomorphism between proofs and
programs, ideas from logic can be transferred into the programming
language community, and programming language problems can motivate new
developments in proof theory. In \citet*{scherer2015} we extended
focusing with a new notion of \emph{saturation}, giving new canonical
representations which had the additional property of being effectively
searchable/enumerable at a given type. While we did not expect this as
a side-result, those enumerable canonical representations finally
solved the open problem of deciding the equivalence in presence of
general finite sums~\citep*{empty-equiv}.

These theoretical results only cover very idealized formal languages,
but those are the basis of our mathematical descriptions of most
real-world programming languages and systems. In particular, they are
closest to richly typed, functional programming languages (Haskell,
SML and OCaml for example), as well as proof assistants -- languages
for mathematical proofs. We will restrict our attention to those
families of languages in the rest of this proposal.

We believe that we are only at the beginning of proof-theoretical
approaches to canonical representations of programs%~\citep*{snapl}
. Promising applications of this work include automatically filling
richly-typed program fragments, and automated equivalence
checking. They would make it easier to write correct software, a major
objective of programming language research.

We propose to push further, both in theory and in practice -- each
informing the other -- with the following objectives for a four-year
period:
\begin{enumerate}
\item Studying canonical representations in richer $\lambda$-calculi,
  to bridge the gap with functional languages and proof assistants
  used today. This is a deep, high-risk theoretical challenge.

\item Uncovering connections with other proof-theoretic approaches to
  the structure of proofs, such as \emph{deep inference} and
  \emph{combinatorial proof}. This is a medium-risk challenge that
  could connect those areas to programming language applications that
  were not on the radar before.

\item Developing practical tools for program equivalence checking in
  functional programming languages. This is a low-risk problem
  with a large potential for applications and user adoption.

\item Using canonical representations, in particular our
  \emph{saturated normal forms}, to reduce the search space in
  \emph{program synthesis} problems. This is a medium-risk challenge;
  our theoretical developments could bring large performance
  improvements to existing program synthesis systems.
\end{enumerate}

The principal investigator comes from a programming-languages
background, but works inside a group with a strong proof-theory
expertise. To our knowledge, this general positioning is unique in the
area (even at the international level); the approaches we suggest to
programming-language applications have shown some early promises, but
are not currently pursued in programming-languages groups due to lack
of theoretical expertise. Conversely, proof-theory groups usually do
not target applications to programming languages; we believe there is
a strong potential for practical impact.

\paragraph{Richer type theories} While simply-typed systems capture
the essence of basic datatypes, existing programming systems use more
advanced types. \emph{Polymorphic types}, which describe genericity
and data abstraction, are the next frontier for canonical
representations, and would let us describe most of today's functional,
statically-typed programming languages such as OCaml, Haskell and
Scala. From a proof-theory perspective, they correspond to
second-order logic. Going even further, one would be interested in
canonical representations of \emph{dependent types}, used in many
proof assistants (Coq, Lean, Agda, Idris, Cedille...), which could
improve their local proof-search engines.

Studying these richer settings is a major challenge because we already
know that equivalence-checking of programs at these types, as well as
proof search in the correspond logics, are undecidable. Any proposal
for canonical representations must be partial -- fail to compute
representations for some program. However, many of the applications we
have in mind for canonical representations, such as equivalence
checking or program synthesis, can accomodate partial procedures: they
remain useful if they sometimes answer ``I don't know'' or time out.

\paragraph{New connections to logic} Proof nets and combinatorial
proofs are an ongoing research programme proposing new representations
of proof in classical and intuitionistic logics, aiming at
canonicity~\citep*{hughes18,lutz18}. We believe that comparing them to
our approach to term canonicity, based on focusing and saturation,
could put new connections to light -- and possibly suggest areas of
application of these fairly theoretical logics to programming
languages. There is a medium risk that the sources of canonicity in
combinatorial proofs are totally inapplicable to our
programming-language setting, if they relies on irreversibly erasing
computational information.

\paragraph{Practical equivalence checking} Some of the changes that
programmers manually perform on a large codebase are ``refactorings'',
reorganizations of the source code that should not change the program
behavior but make future modifications and maintenance easier. From
our experience on canonical forms and equivalence for typed,
functional programming languages, we propose to build an automated
equivalence checker that can reassure a programmer, at the press
a button, that a code change is indeed a valid refactoring.

There is automated tooling support for certain atomic refactoring
operations (rename variable, extract method...), and research to
verify these atomic
operations~\citep*{refactoring-verification-challenge}. But many users
refactor by manually editing the source, several related changes at
a time, and they exchange their modifications as textual patches. We
propose to check the equivalence of the original and patched
programs. Equivalence checking is undecidable in real-world languages,
but refactoring changes are designed to be simple and reviewable by
humans, so they are more likely (than arbitrary instances) to be
supported by partial algorithms.

Equivalence checking has many other practical applications
(for example, after-the-fact validation of compiler optimizations, or
cross-comparison of two compiler versions), so we can hope for some
unplanned side-results of building a practical checker.

\paragraph{Saturation for synthesis} Program synthesis is about
exploring a large search space of candidate programs, testing them
against some sort of specification (input/output example pairs,
a logic formula on their behavior, etc.). There is a growing interest
in type-directed synthesis for functional programming language, and
the experts in the field have (re)discovered the proof-theoretic
notion of \emph{focusing}, which reduces the synthesis search space by
imposing additional structure on candidate
programs~\citep*{%osera1,
osera2,mit}. Their experimental results show
that phase-ordering optimizations suggested by focusing can bring
order-of-magnitude speedup, solving previously-infeasible synthesis
problems.

Our objective is to apply our notion of \emph{saturation}, which has
stronger canonicity properties than focusing alone for pure functional
programs, to reduce the program search space and improve synthesis
performance. There is a real potential for impact with interesting
program synthesis applications, including programming tools for
non-specialists and partially-automated verified programming.

There is a tension in synthesis between being smart and fast: if
a technique reduces the search space but slows down the production of
candidate programs, it may not improve synthesis in
practice. Saturation reduces backtracking, but leads to larger normal
forms: there is a medium risk that it would turn out to be unusable
for synthesis.

% \begin{xcomment}
% Dans cette section, rÃ©pondant au critÃ¨re dâ€™Ã©valuation Â« QualitÃ© et ambition scientifique Â», doivent Ãªtre prÃ©sentÃ©es les informations suivantes :
% \begin{itemize}
% \item Description des objectifs et des hypothÃ¨ses de recherche ;
% \item Positionnement du projet par rapport Ã&nbsp; lâ€™Ã©tat de lâ€™art ;
% \item PrÃ©sentation de la mÃ©thodologie utilisÃ©e pour atteindre les
%   objectifs du projet ;
% \item DÃ©monstration du caractÃ¨re novateur du projet, de son
%   originalitÃ© tant du point de vue des objectifs poursuivis que de la
%   mÃ©thodologie ;
% \item Positionnement du projet par rapport aux enjeux de recherche de
%   lâ€™axe scientifique choisi.
% \end{itemize}
%
% Pour rappel du texte de lâ€™AAPG2019, le critÃ¨re Â«Â&nbsp;QualitÃ© et ambition scientifiqueÂ&nbsp;Â» est un critÃ¨re discriminant, i.e. seuls les projets ayant obtenu la note Â«Â&nbsp;AÂ&nbsp;Â» sur ce critÃ¨re de la part du comitÃ© dâ€™Ã©valuation scientifique peuvent Ãªtre invitÃ©s en Ã©tape 2.
% \end{xcomment}

\vspace{-1em}
\section{Partenariat}
% Partenariat

The principal investigator of the project, Gabriel Scherer, is CR at
INRIA Saclay, in the Parsifal project-team. The project will span over
four years and require one post-doc and one PhD student. Scherer's
colleagues Lutz StraÃŸburger and Dale Miller, also in project-team
Parsifal, would be involved in the project; one of them (depending on
the PhD student's main focus) would also co-supervise the PhD. Project
funding would also help securing collaborations external to INRIA
Saclay, with Guilhem Jaber (INRIA Rennes) and Nadia Polikarpova
(University of California, San Diego).

\paragraph{Principal Investigator} Gabriel Scherer received his PhD in
2016 from the Paris-Diderot University (working at
INRIA Rocquencourt), and spent 18 months as a post-doc at Northeastern
University (Boston), before joining INRIA Saclay in July 2017. He has
published in top conferences (ICFP, LICS, POPL) either alone, with
direct colleagues from the same lab, or remote collaborators. His
expertise is recognized, as witnessed by invitations to chair research
workshops in his community (the OCaml Workshop and the ML
Family workshop) and to serve in program committees (ICFP 2017,
POPL 2018). Gabriel Scherer has a strong programming language
expertise, both in theory and in practice (he is one of the
maintainers of the OCaml programming language implementation).

Gabriel Scherer first started applying logical techniques during his
PhD, and joined the Parsifal team at INRIA Saclay precisely to work
with the strong proof-theory expertise of Parsifal. This JCJC project
will be essential in opening collaborations within his team and
institution, and provide an opportunity to fund and supervise research
on his own research goals.

\paragraph{Collaborators} Our direct colleague Dale Miller is one of
the leading experts on focusing in proof theory, and would be
a natural collaborator for our first objective, ``richer type
theories''.

Our direct colleague Lutz StraÃŸburger is one of the leading experts on
combinatorial proofs, and would be a natural collaborator for our
second objective, ``New connection to logics''.

Natural collaborators for ``Practical equivalence checking'' would be
(1) the ``Trustworthy refactoring'' group at Kent (UK) % TODO URL
which builds software that we could reuse and build upon and (2)
Guilhem Jaber (UniversitÃ© de Nantes), as an expert on semantic
approaches to understand program equivalence in presence of
non-termination, control operators and general references.

Finally, we are in contact with Nadia Polikarpova, one of the leading
experts on program synthesis in rich type systems, and this would be
an excellent opportunity for collaboration.

\paragraph{Funding, Open Access, IP, (no) data} We request
\projectcost{} to fund one PhD scholarship (\EUR{110,000}), a one-year
postdoc (\EUR{65,000}), a travel and equipment budget (\EUR{5,000} per
person-year (8)), and budget to visit or host collaborators
(\EUR{3,000} per project-year (4)).

We plan to distribute our preprints on HAL and release any softare
prototype as free software, following common Open Access
practices. The project will not involve building research databases or
handling personal data of any kind.

% \begin{xcomment}
% Cette section est en lien avec le critÃ¨re dâ€™Ã©valuation Â«Â&nbsp;Organisation et rÃ©alisation du projetÂ&nbsp;Â»Â&nbsp;.

% \paragraph{Sâ€™il sâ€™agit dâ€™un projet jeune chercheure â€“ jeune chercheur (JCJC),}

% PrÃ©senter le coordinateur scientifique, son positionnement au sein de
% son organisme ou laboratoire dâ€™accueil, son expÃ©rience antÃ©rieure en
% termes de coordination et dans le domaine objet de la prÃ©-proposition,
% son implication dans le projet objet de la prÃ©-proposition.

% PrÃ©senter lâ€™Ã©quipe constituÃ©e autour du projet objet de la
% prÃ©-proposition, sa qualitÃ©, sa complÃ©mentaritÃ© dans lâ€™atteinte des
% objectifs prÃ©cÃ©demment Ã©tablis.

% Montrer en quoi le projet objet de la prÃ©-proposition sera facteur
% de prise de responsabilitÃ© du coordinateur et du dÃ©veloppement de son
% Ã©quipe.
% \end{xcomment}

% 110K these (3 ans)
% 130K post-doc (2 ans)
% 515 to 3000/mois stagiaire
% 5K/ans/personne travel + invitations + schools

\vspace{-1em}
\section{Bibliographic references}
% References related to the project

\newcommand{\collab}[1]{\textcolor{blue}{#1}}
\begin{small}
\bibliography{proposal.bib}
\end{small}

\end{document}
</pre></body></html>