@INPROCEEDINGS{tphols2000-Letouzey, crossref = "tphols2000", title = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq", author = "Pierre Letouzey and Laurent Th{\'e}ry", pages = "387--404"} @PROCEEDINGS{tphols2000, editor = "J. Harrison and M. Aagaard", booktitle = "Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000", series = "Lecture Notes in Computer Science", volume = 1869, year = 2000, publisher = "Springer-Verlag"}