From bf142d5058c3767a9fae07f32e98ddbfd3720d1a Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 12 Jan 2015 17:21:48 +0100 Subject: Whodidwhat-8.5: a global pass MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Updating my own work and others when I could think of them. --- doc/whodidwhat/whodidwhat-8.5update.tex | 51 +++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 22 deletions(-) (limited to 'doc/whodidwhat') diff --git a/doc/whodidwhat/whodidwhat-8.5update.tex b/doc/whodidwhat/whodidwhat-8.5update.tex index c187cdb43..ce099dc36 100644 --- a/doc/whodidwhat/whodidwhat-8.5update.tex +++ b/doc/whodidwhat/whodidwhat-8.5update.tex @@ -73,13 +73,17 @@ \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 + 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: Amokrane Saïbi with extensions by Arnaud Spiwack and - Matthieu Sozeau +\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}...): @@ -97,6 +101,7 @@ \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 @@ -108,28 +113,30 @@ \subsection{Predefined tactics} \begin{itemize} -\item Basic tactics (\texttt{intro}, \texttt{apply}, +\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}), with contributions from Hugo Herbelin, Enrico Tassi, ... + 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 + {\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 Refinement (\texttt{refine}): Jean-Christophe Filliâtre \item Introduction patterns: Eduardo Gimenez with collective extensions -\item Forward reasoning: Hugo Herbelin (\texttt{assert}, \texttt{apply in}), Pierre Letouzey (\texttt{specialize}, initial version by Amy Felty) +\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 Tactics about equivalence properties (\texttt{reflexivity}, - \texttt{symmetry}, \texttt{transitivity}): Christine Paulin (?), -\item Equality tactics (\texttt{injection}/\texttt{discriminate}): - Cristina Cornes -\item Inversion tactics (\texttt{inversion}): Cristina Cornes, Chet Murthy \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 @@ -180,11 +187,6 @@ \begin{itemize} \item Program extraction: Pierre Letouzey (first implementation by Benjamin Werner, second by Jean-Christophe Filliâtre) -\item Export of context to external communication tools (\texttt{dp}): - Nicolas Ayache and Jean-Christophe Filliâtre, with contributions by - Claude Marché -\item Export of terms and environments to XML format: Claudio - Sacerdoti Coen, with extensions from Cezary Kaliszyk \end{itemize} \section{Environment management} @@ -229,7 +231,7 @@ \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 +\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 @@ -261,9 +263,6 @@ \section{Graphical interfaces} \begin{itemize} -\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 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 @@ -332,6 +331,14 @@ \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 -- cgit v1.2.3