Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: whodidwhat-8.5update.tex Sprache: Latech

Original von: Coq^©

\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 support: 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}

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.