Pierre Halmagrand

I was a PhD student at LSV (ENS Cachan), member of Deducteam (Inria) and CPR (Cnam/Cedric). My PhD was funded by the ANR project BWare. I am working on formal methods, in particular the B Method, and automated deduction. I am the main developer of the automated theorem prover Zenon Modulo.


Mail: pierre(at)halmagrand(dot)com

PhD Manuscript

Automated Deduction and Proof Certification for the B Method. [pdf]

PhD Defense presentation (in french) [pdf]


International Conferences (with proceedings and committee)

Pierre Halmagrand, Soundly Proving B Method Formulae Using Typed Sequent Calculus. In 13th International Colloquim on Theoretical Aspects of Computing (ICTAC), volume 9965 of Lecture Notes in Computer Science (LNCS). Springer. Taipei, Taiwan, October 2016. [pdf]

Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, and Olivier Hermant. Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. In LPAR 20: 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 35 of EPiC Series in Computing. EasyChair. Suva, Fiji, November 2015. [pdf]

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 8312 of LNCS/ARCoSS. Springer. Stellenbosch, South Africa, December 2013. [pdf]

International Workshops (with proceedings and committee)

Guillaume Bury, Raphael Cauderlier, and Pierre Halmagrand. Implementing Polymorphism in Zenon. In 11th International Workshop on the Implementation of Logics (IWIL), Suva, Fiji, November 2015. [pdf]

Raphael Cauderlier and Pierre Halmagrand. Checking Zenon Modulo Proofs in Dedukti. In Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Berlin, Germany, August 2015. [pdf]

Pierre Halmagrand. Using Deduction Modulo in Set Theory. In SETS14, 1st International Workshop about Sets and Tools, EasyChair. Toulouse, France, June 2014. [pdf]

David Delahaye, Damien Doligez, Frederic Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. In International Workshop on the Implementation of Logics (IWIL). Stellenbosch, South Africa, December 2013. [pdf]