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.
Order theory in Coq using the type classes mechanism and in
particular the new "setoid" rewriting tactic based on classes.
Some category theory in Coq using the type classes mechanism.
Type-safe sprintf using delimited continuations in Coq. Requires
Prelude.
A formalization of the Finger Tree datastructure in Coq. Requires
Prelude and Safe.
This is a port of the Haskell prelude implementations of the usual
functors, applicative and monad structures.
Safe (dependently-typed) list combinators.
A formalization of the Celebrities problem proposed by Richard
Bird .
A certified implementation of the quicksort algorithm.
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.
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.
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, Hsiang-Shang Ko & 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.
A dependently-typed formalization of simply-typed lambda-calculus: substitution, denotation, normalization. Matthieu Sozeau, Unpublished, 2007 - Literate Coq script.
