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/misc/AoP

A port of the "Algebra of Programming Using
Dependent Types" [1] paper, using "setoid" rewriting
and type classes.

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 .

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 [2]
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).

Copyright © 2006-2015 Matthieu Sozeau