diff options
Diffstat (limited to 'doc/whodidwhat/whodidwhat-8.5update.tex')
| -rw-r--r-- | doc/whodidwhat/whodidwhat-8.5update.tex | 346 |
1 files changed, 346 insertions, 0 deletions
diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex new file mode 100644 index 00000000..ce099dc3 --- /dev/null +++ b/doc/whodidwhat/whodidwhat-8.5update.tex @@ -0,0 +1,346 @@ +\documentclass{article} + +\usepackage{fullpage} +\usepackage[utf8]{inputenc} +\usepackage{t1enc} + +\begin{document} + +\title{Who did what in the Coq archive?} + +\author{The Coq development team} + +\maketitle + +\centerline{(updated for Coq 8.5)} + +\section{The Calculus of Inductive Constructions} + +\begin{itemize} +\item The Calculus of Constructions + \begin{itemize} + \item Core type-checker: Gérard Huet and Thierry Coquand with + optimizations by Chet Murthy, Bruno Barras + \item Head reduction functions: Gérard Huet, Christine Paulin, Bruno Barras + \end{itemize} +\item Conversion and reduction + \begin{itemize} + \item Lazy conversion machine: Bruno Barras + \item Transparency/opacity: Bruno Barras + \item Bytecode-based conversion: Benjamin Grégoire + \item Binary-words retroknowledge: Arnaud Spiwack + \item Native code based conversion: Maxime Dénès, Benjamin Grégoire + \end{itemize} +\item The universe hierarchy + \begin{itemize} + \item Floating universes: Gérard Huet, with contributions from Bruno Barras + \item Algebraic universes: Hugo Herbelin + \end{itemize} +\item Mutual inductive types and recursive definitions + \begin{itemize} + \item Type-checking: Christine Paulin + \item Positivity condition: Christine Paulin + \item Guardness condition for fixpoints: Christine Paulin; + extensions by Eduardo Gimenez, Bruno Barras, Pierre Boutillier; fixes by + Bruno Barras, Maxime Dénès + \item Recursively non-uniform parameters: Christine Paulin + \item Sort-polymorphism of inductive types: Hugo Herbelin + \end{itemize} +\item Local definitions: Hugo Herbelin +\item Mutual coinductive types and corecursive definitions: Eduardo Gimenez +\item Module system + \begin{itemize} + \item Core system: Jacek Chrz\k{a}szcz + \item Inlining: Claudio Sacerdoti Coen and Élie Soubiran + \item Module inclusion: Élie Soubiran + \item Functorial signature application: Élie Soubiran + \item Transparent name space: Élie Soubiran + \item Resolution of qualified names: Hugo Herbelin + \item Operator for nested functor application: Élie Soubiran and + Pierre Letouzey + \end{itemize} +\item Minimalist stand-alone type-checker (\texttt{coqchk}): Bruno Barras, with extra support for modules by Élie Soubiran and Pierre Letouzey +\item Eta-conversion: Hugo Herbelin, with contributions from Stéphane + Glondu, Benjamin Grégoire +\end{itemize} + +\section{Specification language} + +\begin{itemize} +\item Sections: Gilles Dowek with extra contributions by Gérard + Huet, Chet Murthy, Hugo Herbelin +\item The \texttt{Russell} specifications language, proof obligations (\texttt{Program}): Matthieu Sozeau +\item Type inference: Chet Murthy, with extra contributions by Bruno + Barras, Hugo Herbelin, Matthieu Sozeau, Enrico Tassi +\item Pattern-matching: Hugo Herbelin on top of a first version by + Cristina Cornes, contributions by Arnaud Spiwack +\item Implicit arguments: Amokrane Saïbi, with extensions by Hugo + Herbelin, Matthieu Sozeau, Pierre Boutillier +\item Synthetic {\tt Arguments} command: Enrico Tassi +\item Coercions: Amokrane Saïbi +\item Records + \begin{itemize} + \item Core implementation: Amokrane Saïbi with extensions by Matthieu Sozeau + \item Extension to inductive and co-inductive records: Arnaud Spiwack + \item Non-recursive variants: Arnaud Spiwack + \end{itemize} +\item Canonical structures: Amokrane Saïbi +\item Type classes: Matthieu Sozeau +\item Function (\texttt{Function}, \texttt{functional induction}...): + Julien Forest (preliminary versions by Pierre Courtieu + (\texttt{Functional Schemes}) and Yves Bertot (\texttt{Recursive + Definition})) +\item Generation of induction schemes: Christine Paulin, Vincent + Siles, Matthieu Sozeau + \end{itemize} + +\section{Tactics} + +\subsection{General tactic support} + +\begin{itemize} +\item Proof engine: Arnaud Spiwack (first version by Thierry Coquand, second version by Chet Murthy) +\item Ltac: David Delahaye, with extensions by Hugo Herbelin, Bruno Barras, ... + Evolution to the new proof engine Arnaud Spiwack, Pierre-Marie P\'edrot +\item Tactic notations: Hugo Herbelin (first version by Chet Murthy) +\item Main tactic unification procedure: Chet Murthy with + contributions from Hugo Herbelin and Matthieu Sozeau +\item Mathematical-style language (C-Zar): Pierre Corbineau +\item Communication with external tools (\texttt{external}): Hugo Herbelin +\item Proof structuring (bullets and brackets): Arnaud Spiwack +\end{itemize} + +\subsection{Predefined tactics} + +\begin{itemize} +\item Basic refinement tactic (\texttt{refine}): Arnaud Spiwack (previous non-basic version by Jean-Christophe Filliâtre) +\item Core tactics (\texttt{intro}, \texttt{apply}, + \texttt{assumption}, \texttt{exact}): Thierry Coquand, with further + collective extensions +\item Reduction tactics: Christine Paulin (\texttt{simpl}), Bruno + Barras (\texttt{cbv}, \texttt{lazy}), Pierre Boutillier (\texttt{cbn}) + with contributions from Hugo Herbelin, Enrico Tassi, ... +\item Tacticals: Thierry Coquand, Chet Murthy, Eduardo Gimenez, ...; + new versions of {\tt info} and {\tt Show Script} by Pierre Letouzey; + {\tt timeout} by Pierre Letouzey; backtracking-related tacticals by Arnaud Spiwack +\item Generic tactic traces ({\tt Info}) by Arnaud Spiwack (based on the former {\tt info} tactical) +\item Induction: Christine Paulin (\texttt{elim}, \texttt{case}), Hugo Herbelin (\texttt{induction}, \texttt{destruct} +\item Introduction patterns: Eduardo Gimenez with collective extensions +\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{enough}, \texttt{apply in}), + Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\item Rewriting tactics (\texttt{rewrite}): basic version by Christine Paulin, + extensions by Jean-Christophe Filliâtre and Pierre Letouzey +\item Setoid rewriting: Matthieu Sozeau (first version by Clément + Renard, second version by Claudio Sacerdoti Coen), contributions + from Nicolas Tabareau +\item Tactics about equivalence properties (\texttt{reflexivity}, + \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), +\item Equality tactics (\texttt{injection}/\texttt{discriminate}): Cristina Cornes, extensions by Hugo Herbelin +\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy +\item Decision of equality: Eduardo Gimenez +\item Basic Ltac-level tactics: Pierre Letouzey, Matthieu Sozeau, + Evgeny Makarov +\item Tactics about existential variables: Clément Renard, Pierre Corbineau, Stéphane Glondu, Arnaud Spiwack, ... +\end{itemize} + +\subsection{General automation tactics} + +\begin{itemize} +\item Resolution (\texttt{auto}, \texttt{trivial}): Christine Paulin + with extensions from Chet Murthy, Eduardo Gimenez, Patrick + Loiseleur (hint bases), Matthieu Sozeau +\item Resolution with existential variables (\texttt{eauto}): Chet Murthy, Jean-Christophe Filliâtre, with extensions from Matthieu Sozeau +\item Automatic rewriting (\texttt{autorewrite}): David Delahaye +\end{itemize} + +\subsection{Domain-specific decision tactics} + +\begin{itemize} +\item Congruence closure (\texttt{cc}): Pierre Corbineau +\item Decision of first-order logic (\texttt{firstorder}): Pierre Corbineau +\item Simplification of polynomial fractions (\texttt{field}): Laurent + Théry and Benjamin Grégoire (first version by David Delahaye and + Micaela Mayero) +\item Simplification of polynomial expressions (\texttt{ring}): Assia + Mahboubi, Bruno Barras and Benjamin Grégoire (first version by + Samuel Boutin, second version by Patrick Loiseleur) +\item Decision of systems of polynomial equations: Loïc Pottier (\texttt{nsatz}) +\item Decision of systems of linear inequations: Frédéric Besson + (\texttt{psatzl}); Loïc Pottier (\texttt{fourier}) +\item Decision of systems of linear inequations over integers: + Frédéric Besson (\texttt{lia}); Pierre Crégut (\texttt{omega} and + \texttt{romega}) +\item (Partial) decision of systems of polynomical inequations + (\texttt{sos}, \texttt{psatz}): Frédéric Besson, with generalization + over arbitrary rings by Evgeny Makarov; uses HOL-Light interface to + \texttt{csdp} by John Harrisson +\item Decision/simplification of intuitionistic propositional logic: + David Delahaye (\texttt{tauto}, \texttt{intuition}, first version by + Cesar Mu\~noz, second version by Chet Murthy), with contributions + from Judicaël Courant; Pierre Corbineau (\texttt{rtauto}) +\item Decision/simplification of intuition first-order logic: Pierre + Corbineau (\texttt{firstorder}) +\end{itemize} + +\section{Extra tools} + +\begin{itemize} +\item Program extraction: Pierre Letouzey (first implementation by + Benjamin Werner, second by Jean-Christophe Filliâtre) +\end{itemize} + +\section{Environment management} + +\begin{itemize} +\item Separate compilation: initiated by Chet Murthy +\item Import/Export: initiated by Chet Murthy +\item Options management: Hugo Herbelin with contributions by Arnaud Spiwack +\item Resetting and backtracking: Chet Murthy with contributions from Pierre Courtieu +\item Searching: Hugo Herbelin and Yves Bertot with extensions by Matthias Puech +\item Whelp suppport: Hugo Herbelin +\end{itemize} + +\section{Parsing and printing} + +\begin{itemize} +\item General parsing support: Chet Murthy, Bruno Barras, Daniel de Rauglaudre +\item General printing support: Chet Murthy, Jean-Christophe Filliâtre +\item Lexing: Daniel de Rauglaudre +\item Support for UTF-8: Hugo Herbelin, with contributions from Alexandre Miquel and Yann Régis-Gianas +\item Numerical notations: Hugo Herbelin, Patrick Loiseleur, Micaela Mayero +\item String notations: Hugo Herbelin +\item New ``V8'' syntax: Bruno Barras, Hugo Herbelin with contributions by Olivier Desmettre +\item Abbreviations: Chet Murthy +\item Notations: Chet Murthy, Hugo Herbelin +\end{itemize} + +\section{Libraries} + +\begin{itemize} +\item Init: collective (initiated by Christine Paulin and Gérard Huet) +\item Arith: collective (initiated by Christine Paulin) +\item ZArith: collective (initiated by Pierre Crégut) +\item Bool: collective (initiated by Christine Paulin) +\item NArith: Hugo Herbelin, Pierre Letouzey, Evgeny Makarov (out of + initial contibution by Pierre Crégut) +\item Lists: Pierre Letouzey, Jean-Marc Notin (initiated by Christine Paulin) +\item Vectors: Pierre Boutillier +\item Reals: Micaela Mayero (axiomatization and main properties), Olivier Desmettre (convergence, derivability, integrals, trigonometric functions), contributions from Russell O'Connor, Cezary Kaliszyk, Guillaume Melquiond, Yves Bertot, Guillaume Allais +\item Relations: Bruno Barras, Cristina Cornes with contributions from + Pierre Castéran +\item Wellfounded: Bruno Barras, Cristina Cornes +\item FSets: Pierre Letouzey, from initial work with Jean-Christophe Filliâtre, decision tactic for FSets by Aaron Bohannon, red-black trees by Andrew Appel and Pierre Letouzey +\item MSets: Pierre Letouzey +\item Logic: Christine Paulin, Hugo Herbelin, Bruno Barras, contributions by Arnaud Spiwack +\item Numbers: Evgeny Makarov (abstractions), Laurent Théry and Benjamin Grégoire (big numbers), Arnaud Spiwack and Pierre Letouzey (word-based arithmetic), further extensions by Pierre Letouzey; integration of Arith and ZArith to Numbers by Pierre Letouzey +\item Classes: Matthieu Sozeau +\item QArith: Pierre Letouzey, with contributions from Russell O'Connor +\item Setoid: Matthieu Sozeau (first version by Clément Renard, second version by Claudio Sacerdoti Coen) +\item Sets: Gilles Kahn and Gérard Huet +\item Sorting: Gérard Huet with revisions by Hugo Herbelin +\item Strings: Laurent Théry +\item Program: Matthieu Sozeau +\item Unicode: Claude Marché +\end{itemize} + +\section{Commands} + +\begin{itemize} +\item Batch compiler (\texttt{coqc}): Chet Murthy (?) +\item Compilation dependency calculator (\texttt{coqdep}): + Jean-Christophe Filliâtre +\item Statistic tool (\texttt{coqwc}): Jean-Christophe Filliâtre +\item Simple html presentation tool (\texttt{gallina}) (deprecated): Jean-Christophe Filliâtre +\item Auto-maker (\texttt{coq\_makefile}): Jean-Christophe Filliâtre, + with contributions from Judicaël Courant, updated by Pierre Boutillier +\item LaTeX presentation tool (\texttt{coq-tex}): Jean-Christophe Filliâtre +\item Multi-purpose presentation tool (\texttt{coqdoc}): Jean-Christophe Filliâtre with extensions from + Matthieu Sozeau, Jean-Marc Notin, Hugo Herbelin and contributions from Adam Chlipala +\item Interactive toplevel (\texttt{coqtop}): Jean-Christophe Filliâtre (?) +\item Custom toplevel builder (\texttt{coqmktop}): Jean-Christophe Filliâtre (?) +\end{itemize} + +\section{Graphical interfaces} + +\begin{itemize} +\item Support for {\em Proof General}: Pierre Courtieu with contributions from Arnaud Spiwack +\item {\em CoqIDE}: Benjamin Monate with contributions from + Jean-Christophe Filliâtre, Claude Marché, Pierre Letouzey, Julien + Narboux, Hugo Herbelin, Pierre Corbineau, Pierre Boutillier, + Pierre-Marie Pédrot; processus-based communication protocol by + Vincent Gross with contributions from Pierre Letouzey, Pierre + Boutillier, Pierre-Marie Pédrot; backtracking revised by Pierre + Letouzey; uses the Cameleon library by Maxence Guesdon; +\end{itemize} + +\section{Architecture} + +\begin{itemize} +\item Functional-kernel-based architecture: Jean-Christophe Filliâtre +\item Extensible objects and summaries: Chet Murthy +\item Hash-consing: Bruno Barras +\item Error locations: Jean-Christophe Filliâtre, Bruno Barras, Hugo Herbelin, with contributions from Arnaud Spiwack +\item Existential variables engine: Chet Murthy with revisions by + Bruno Barras and Arnaud Spiwack and extensions by Clément Renard and + Hugo Herbelin +\end{itemize} + +\section{Development tools} + +\begin{itemize} +\item Makefile's: Chet Murthy, Jean-Christophe Filliâtre, Judicaël + Courant, Lionel Mamane, Pierre Corbineau, Pierre Letouzey with + contributions from Stéphane Glondu, Hugo Herbelin, ... +\item Debugging: Jean-Christophe Filliâtre with contributions from Jacek Chrz\k{a}szcz, Hugo Herbelin, Bruno Barras, ... +\item ML quotations: David Delahaye and Daniel de Rauglaudre +\item ML tactic and vernacular extensions: Hugo Herbelin (first version by Chet Murthy) +\item Test suite: collective content, initiated by Jean-Christophe Filliâtre with further extensions by Hugo Herbelin, Jean-Marc Notin +\end{itemize} + +\section{Maintenance and system engineering} + +\begin{itemize} +\item General bug support: Gérard Huet, Christine Paulin, Chet Murthy, + Jean-Christophe Filliâtre, Hugo Herbelin, Bruno Barras, Pierre + Letouzey with contributions at some time from Benjamin Werner, + Jean-Marc Notin, Pierre Boutillier, ... +\item Team coordination: Gérard Huet, Christine Paulin, Hugo Herbelin, + with various other contributions +\item Packaging tools: Henri Laulhere, David Delahaye, Julien Narboux, + Pierre Letouzey, Enrico Tassi (Windows); Damien Doligez, Hugo + Herbelin, Pierre Boutillier (MacOS); Jean-Christophe Filliâtre, + Judicaël Courant, Hugo Herbelin, Stéphane Glondu (Linux) +\end{itemize} + +\section{Documentation} + +\begin{itemize} + +\item Reference Manual: collective, layout by Patrick Loiseleur, + Claude Marché (former User's Guide in 1991 by Gilles Dowek, Amy + Felty, Hugo Herbelin, Gérard Huet, Christine Paulin, Benjamin + Werner; initial documentation in 1989 by Thierry Coquand, Gilles + Dowek, Gérard Huet, Christine Paulin), +\item Basic tutorial: Gérard Huet, Gilles Kahn, Christine Paulin +\item Tutorial on recursive types: Eduardo Gimenez with updates by Pierre Castéran +\item FAQ: Hugo Herbelin, Julien Narboux, Florent Kirchner +\end{itemize} + +\section{Features discontinued by lack of support} + +\begin{itemize} +\item Searching modulo isomorphism: David Delahaye +\item Explanation of proofs in pseudo-natural language: Yann Coscoy +\item Export of context to external communication tools (\texttt{dp}): + Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by + Claude Marché +\item Support for {\em PCoq}: Yves Bertot with contributions by + Laurence Rideau and Loïc Pottier; additional support for {\em TmEgg} + by Lionel Mamane +\item Export of terms and environments to XML format: Claudio + Sacerdoti Coen, with extensions from Cezary Kaliszyk +\end{itemize} + +For probable oversights or accidental errors, please report to Hugo~\verb=.=~Herbelin~\verb=@=~inria~\verb=.=~fr + +\end{document} |