\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)
¤
|
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.
|