[3] Denis Cousineau, David Mentré, and Hiroaki Inoue. Automated deductive verification for Ladder programming. CoRR, abs/1912.10629, 2019. [ bib | http ]
[2] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium on Formal Methods, volume 7436 of Lecture Notes in Computer Science, pages 147--154. Springer, 2012. [ bib | full text on HAL ]
[1] Denis Cousineau and Olivier Hermant. A semantic proof that reducibility candidates entail cut elimination. In Ashish Tiwari, editor, 23nd International Conference on Rewriting Techniques and Applications, volume 15 of Leibniz International Proceedings in Informatics, pages 133--148, Nagoya, Japan, 2012. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | full text on HAL ]