darcs get http://mattam.org/repos/coq/misc/AoP
A port of the "Algebra of Programming Using
Dependent Types" [1] paper, using "setoid" rewriting
and type classes.
Coq stuff
Coq is an interactive theorem prover made for formalizing
mathematical theories and algorithms using type theory. I am fond of
using it to prove everything that is shown to me and I don't
understand at first. So here's a list of Coq stuff I use to prove
things and some developments.
darcs get http://mattam.org/repos/coq/order
Order theory in Coq using the type classes mechanism and in
particular the new "setoid" rewriting tactic based on classes.
darcs get http://mattam.org/repos/coq/cat
Some category theory in Coq using the type classes mechanism.
Type-safe sprintf using delimited continuations in Coq. Requires
Prelude.
darcs get http://mattam.org/repos/coq/fingertrees
A formalization of the Finger Tree datastructure in Coq. Requires
Prelude and Safe.
darcs get http://mattam.org/repos/coq/prelude
This is a port of the Haskell prelude implementations of the usual
functors, applicative and monad structures.
darcs get http://mattam.org/repos/coq/misc/celebs
A formalization of the Celebrities problem proposed by Richard
Bird [2].
darcs get http://mattam.org/repos/coq/misc/sort
A certified implementation of the quicksort algorithm.
darcs get http://mattam.org/repos/coq/misc/nbe
I developed a complete formalization [3]
of simply-typed lambda calculus with constants in the dependently-typed style with the help of Program.
It includes a tait-style proof of weak normalization.
darcs get http://mattam.org/repos/coq/misc/kripke
A formalization of simply-typed lambda calculus and its proof of
normalization using a kripke model. Includes a proof that peirce's
law is not derivable using models and the syntactic characterization
of normal forms. This is joint work with Thorsten Altenkirch.
darcs get http://mattam.org/repos/coq/Russell
A proof of subject-reduction and equivalence between the
declarative and an algorithmic presentation of the type system of
Russell (a Calculus of Constructions with dependent sums and some subtyping).
Algebra of Programming Using Dependent Types in Mathematics of Program Construction. Shin-Cheng Mu and Hsiang-Shang Ko and Patrik Jansson. Philippe Audebaud and Christine Paulin-Mohring (Eds). Volume 5133 of Lecture Notes in Computer Science . Berlin Heidelberg : Springer-Verlag , July 2008, pp.268-283.
Functional Pearls: Finding celebrities: A lesson in functional programming.. Richard S. Bird and Sharon A. Curtis J. Funct. Program. 16 (1), 2006, pp.13-20.
A dependently-typed formalization of simply-typed lambda-calculus: substitution, denotation, normalization. Matthieu Sozeau, Unpublished, 2007 - Literate Coq script.
