Add papers and talks.

.gitignore

@@ -1,7 +1,9 @@
 *.vo
 *.glob
+*.pdf
+*.crashcoqide
+tmp.*
 src/deps
 src/.sconsign.dblite
 coqidescript
 coqdoc
-*.crashcoqide

LICENSE

@@ -1 +1 @@
-All authors involved in the creation of the contents of this package have agreed to release their respective contributions into the Public Domain.
+All authors involved in the creation of the contents of this package have agreed to release their respective contributions into the Public Domain except where noted otherwise.

papers/itp10-roughdiamond/README.txt

@@ -0,0 +1,21 @@
+We use lhs2TeX [1] for the preparation of our paper. lhs2TeX is a preprocessor which takes 
+almost-TeX as input and produces TeX as output.
+
+See compile.sh for how we invoke lhs2TeX and pdflatex.
+
+As you can see, processed.tex is the result of running lhs2TeX on our hand-crafted almost-TeX 
+(paper.tex). It, together with
+  - abstract.ltx
+  - macros.sty
+  - paper.bib
+  - llncs.cls
+  - splncs.bst
+, are compiled by pdflatex to produce the final pdf (paper.pdf).
+
+We provide paper.tex so that, should there be a problem with processed.tex, the latter can be 
+regenerated from paper.tex using lhs2TeX.
+
+The version of lhs2TeX we used is 1.13, but it should not matter, because processed.tex should 
+not depend on lhs2TeX in any way.
+
+[1] http://people.cs.uu.nl/andres/lhs2tex/

papers/itp10-roughdiamond/coq2tex.tex

@@ -0,0 +1,64 @@
+%include polycode.fmt
+
+%format pipe = "\mathopen{|}"
+
+%format times = "\times"
+
+%format hack = "\vspace*{-12ex}"
+%format . = "."
+%format forall = "\forall"
+%format Fixpoint = "\mathbf{Fixpoint}"
+%format Definition = "\mathbf{Definition}"
+%format Eval = "\mathbf{Eval}"
+%format Notation = "\mathbf{Notation}"
+%format Lemma = "\mathbf{Lemma}"
+%format Proof = "\mathbf{Proof}"
+%format Defined = "\mathbf{Defined}"
+%format Function = "\mathbf{Function}"
+%format Proposition = "\mathbf{Proposition}"
+%format Record = "\mathbf{Record}"
+%format Program = "\mathbf{Program}"
+%format Inductive = "\mathbf{Inductive}"
+%format Theorem = "\mathbf{Theorem}"
+%format Let = "\mathbf{Let}"
+%format Variable = "\mathbf{Variable}"
+%format Variables = "\mathbf{Variables}"
+%format measure = "\mathbf{measure}"
+%format Infix = "\mathbf{Infix}"
+%format Class = "\mathbf{Class}"
+%format Instance = "\mathbf{Instance}"
+%format Global = "\mathbf{Global}"
+%format scope = "\mathbf{scope}"
+%format --> = "\longrightarrow"
+%format → = "\rightarrow"
+%format ⟶ = "\longrightarrow"
+
+%format prod = "\hspace{-1mm}\times\hspace{-1mm} "
+%format sp = "\ "
+
+%format == = "= "
+%format /= = "\ne "
+  % Without these, lhs2tex uses three-line equal signs.
+
+%format fcmp = "\circ"
+%format match = "\mathbf{match}"
+%format with = "\mathbf{with}"
+%format end = "\mathbf{end}"
+%format fun = "\lambda\hspace{-1mm} "
+%format nat = "\mathbb{N}"
+%%%format R = "\mathbb{R}"
+%format exists = "\exists "
+%format over = "\mathbf{over}"
+%format INR (a) = a
+%format /\ = "\wedge "
+%format \/ = "\vee"
+%format <-> = "\leftrightarrow "
+%format ==> = "\Longrightarrow "
+%format MonoidMonadTrans.M = "\Varid{MMT}"
+%format NatAddMonoid = (nat, 0, +)
+
+%format { = "\hspace*{0mm}\{"
+%format ` = "\hspace*{0mm}`"
+
+%format `In` = "\in"
+%format `NotIn` = "\notin"

papers/itp10-roughdiamond/roughdiamond.tex

@@ -0,0 +1,114 @@
+\documentclass{llncs}
+\usepackage{url}
+\usepackage{bbm}
+\usepackage[utf8x]{inputenc}
+\newcommand{\N}{\ensuremath{\mathbbm{N}}}
+\newcommand{\Z}{\ensuremath{\mathbbm{Z}}}
+\newcommand{\Q}{\ensuremath{\mathbbm{Q}}}
+%include coq2tex.tex
+\arrayhs %i.e. no page breaks in code blocks
+\divide\abovedisplayskip 4
+\divide\belowdisplayskip 4
+\begin{document}
+\title{Developing the Algebraic Hierarchy with Type Classes in Coq}
+\author{Bas Spitters \and Eelis van der Weegen}
+\institute{Radboud University Nijmegen}
+\maketitle
+\begin{abstract}
+We present a new formalization of the algebraic hierarchy in Coq, exploiting its new type class mechanism to make practical a solution formerly thought infeasible. Our approach addresses both traditional challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which abstraction penalties inhibiting efficient computation are reduced to a bare minimum. To support mathematically sound abstract interfaces for $\N$, $\Z$, and $\Q$, our formalization includes portions of category theory and multisorted universal algebra.
+\end{abstract}
+
+\section{Introduction}
+The development of libraries for formalized mathematics presents many software engineering challenges~\cite{C-corn,DBLP:conf/types/HaftmannW08}, because it is far from obvious how the clean, idealized concepts from everyday mathematics should be represented using the facilitities provided by concrete theorem provers and their formalisms, in a way that is both mathematically faithful and convenient to work with.
+
+For the algebraic hierarchy---a critical component in any library of formalized mathematics---these challenges include structure inference, handling of multiple inheritance, idiomatic use of notations, and convenient algebraic manipulation.
+
+Several solutions have been proposed for the Coq theorem prover: dependent records~\cite{DBLP:journals/jsc/GeuversPWZ02} (a.k.a. telescopes), packed classes~\cite{Packed}, and occasionally modules. We present a new approach based entirely on Coq's new type class mechanism, and show how its features together with a key design pattern let us effectively address the challenges mentioned above.
+
+Since we intend to use this development as a basis for constructive analysis with practical certified exact real arithmetic, an additional objective and motivation in our design is to facilitate \emph{efficient} computation. In particular, we want to be able to effortlessly swap implementations of number representations. Doing this requires that we have clean abstract interfaces, and mathematics tells us what these should look like: we represent $\N$, $\Z$, and $\Q$ as \emph{interfaces} specifying an initial semiring, an initial ring, and a field of integral fractions, respectively.
+
+To express these elegantly and without duplication, our development\footnote{The sources are available
+at:~\url{http://www.eelis.net/research/math-classes/}} includes an integrated formalization of parts of category theory and multi-sorted universal algebra, all expressed using type classes for optimum effect.
+
+% In
+% Coq, type classes have advantages over modules\footnote{
+% Modules are sections on steroids: namespace management, notations, hints, etc.
+% The [Import] command imports all the constants from a module. Thus allowing the user to type B
+% instead of A.B
+% }:
+% they are first class and extract~\cite{letouzey02} to Haskell\footnote{
+% Would module like extraction be possible?}.
+
+\section{The Type-Classified Algebraic Hierarchy}\label{classes}
+
+Unlike Haskell's and Isabelle's second class type classes, Coq's type classes are first class: classes and their instances are realized as ordinary record types (``dictionaries'') and registered constants of these types.
+
+We represent each structure in the algebraic hierarchy as a type class. This immediately leads to the familiar question of which components of the structure should become parameters of the class, and which should become fields. By far the most important design choice in our development is the decision to turn all \emph{structural} components (i.e. carriers, relations, and operations) into parameters, keeping only \emph{properties} as fields. Type classes defined in this way are essentially predicates with automatically resolved proofs.
+
+Conventional wisdom warns that while this approach is theoretically very flexible, one risks extreme inconvenience both in having to declare and pass around all these structural components all the time, as well as in losing notations (because we no longer project named operations out of records).
+
+These are legitimate concerns that we avoid by exploiting the way Coq type classes and their support infrastructure work, using \emph{operational type classes}: classes with a single field representing a single relation or operation in isolation. Such classes are treated specially by Coq in being translated to mere definitions rather than records, with the field projection becoming the identity function.
+\begin{code}
+ Class Equiv A := equiv: relation A.
+ Infix "=" := equiv (at level 70, no associativity).
+\end{code}
+These operational type classes serve to establish \emph{canonical names}, which not only lets us bind notations to them, but also makes their declaration and use implicit in most contexts. For instance, using the following definition of semirings, all structural parameters (represented by operational classes declared with curly brackets) will be implicitly resolved by the type class mechanism rather than listed explicitly whenever we talk about semirings.
+\begin{code}
+Class SemiRing A {e: Equiv A}{plus: RingPlus A}{mult: RingMult A}
+                 {zero: RingZero A}{one: RingOne A}:Prop :=
+  { semiring_mult_monoid:> Monoid A (op:=mult)(unit:=one)
+  ; semiring_plus_monoid:> Monoid A (op:=plus)(unit:=zero)
+  ; semiring_plus_comm:> Commutative plus
+  ; semiring_mult_comm:> Commutative mult
+  ; semiring_distr:> Distribute mult plus
+  ; mult_0_l: forall x, 0 * x == 0 }.
+\end{code}
+The two key Coq features that make this work are implicit quantification (when declaring a semiring), and maximally inserted implicit arguments (when stating that something is a semiring, and when referencing operations and relations). Both were added specifically to support type classes.
+
+Having argued that the \emph{all-structure-as-parameters} approach \emph{can} be made practical, we enumerate some of the benefits that make it worthwhile.
+
+First, multiple inheritance becomes trivial: |SemiRing| inherits two |Monoid| structures on the same carrier and setoid relation, using ordinary named arguments (rather than dedicated extensions~\cite{DBLP:conf/types/Luo08}) to achieve ``manifest fields''.
+
+Second, because our terms are small and independent and never refer to proofs, we are invulnerable to concerns about efficiency and ambiguity of projection paths that plague existing solutions, obviating the need for extensions like the proposed coercion pullbacks~\cite{Hints}.
+
+Third, since our structural type classes are mere predicates, overlap between their instances is a non-issue. Together with the previous point, this gives us tremendous freedom to posit multiple structures on the same operations and relations, including ones derived implicitly via subclasses: by simply declaring a |SemiRing| class instance showing that a ring is a semiring, results about semirings immediately apply implicitly to any known ring, without us having to explicitly encode this relation in the hierarchy definition itself, and without needing any projection or translation of carriers or operations.
+
+\section{Category Theory and Universal Algebra}\label{interfaces}\label{modul}
+
+Motivated originally by our desire to cleanly express interfaces for basic numeric data types such as $\N$ and $\Z$ in terms of their categorical characterization as initial objects in the categories of semirings and rings, respectively, we initially introduced only the very basics of category theory into our development, again using type classes where possible to achieve the same benefits mentioned before.
+
+Realizing that much code duplication for the various algebraic structures in the hierarchy could be avoided by employing universal algebra constructions, we then proceeded to formalize some of the theory of multisorted universal algebra and equational theories, using it to automatically construct varieties of algebras. We avoided existing formalizations~\cite{DBLP:conf/tphol/Capretta99,dominguez2008formalizing} of universal algebra, because we aimed to find out what level of elegance, convenience, and integration can be achieved using the state of the art technology (of which type classes are the most important instance).
+
+At the time of writing, our development includes a fully integrated formalization of a nontrivial portion of category theory and multisorted universal algebra, including various categories (e.g.\ the category |Cat| of categories, and generic variety categories which we instantiate to obtain the categories of monoids, semirings, and rings), functors (including automatically generated forgetful functors), natural transformations, adjunctions, initial models of equational theories constructed from term algebras, transference of proofs between isomorphic models of equational theories, subalgebras, congruences, quotients, products, and the first homomorphism theorem.
+
+There is an interesting interplay in our development between concrete algebraic structure type classes and their expressions on the one hand, and models of universal algebras and varieties instantiated with equational theories on the other. While occasionally a source of tension in that translation in either direction is not (yet) fully automatic, this duality also opens the door to the possibility of fully internalized implementations of generic tactics for algebraic manipulation, no longer requiring plugins. One missing piece in this puzzle is automatic quotation of concrete expressions into universal algebra expressions. We have already implemented a proof of concept showing that like unification hints~\cite{Hints}, type classes can be used to implement Ltac/OCaml-free quotation.
+
+%There is a slight problem when defining the forgetful functor from the category of
+%$\Sigma$-algebras to Sets. This problem is caused by our use of the category of all
+%categories\footnote{Perhaps we should have used higher categories for this.}.
+%We conjecture that this problem disappears when Coq's universe polymorphism is extended to
+%definitions.
+
+% We encourage more efficient implementations by assigning the default implementation a
+% low priority. For example, the distance function on the natural numbers, which is derived from its
+% semiring structure, is assigned priority 10.
+% \begin{code}
+%   Global Program Instance: NatDistance N | 10 := ...
+% \end{code}
+%
+
+\section{Conclusions}
+
+Our development (which according to \texttt{coqwc} consists of about 5K lines of specifications and 1K lines of proofs) shows that the first class type class implementation in Coq is already an extremely powerful piece of technology which enables new practical and elegant solutions to old problems.
+
+In our work we push the type class implementation and the new generalized rewriting infrastructure~\cite{Setoid-rewrite} to their limits, revealing both innocent bugs as well as more serious issues (concerning both efficiency and functionality) that the Coq development team is already working on (for instance with the soon to be revealed new proof engine).
+
+
+
+
+\paragraph{Acknowledgements.}
+We would like to thank Matthieu Sozeau for discussions and quickly solving numerous small bugs and
+feature requests.
+\bibliographystyle{plain}
+\bibliography{alg}
+\end{document}