An informal workshop will take place at ITU (Copenhagen) during March 12-13, on the general topic of certificates. Although most talks will be about proof theory and logical frameworks, we seek to have discussions on the more general notion of certificate, notably in complex security contexts such as e-voting. Several people from Parsifal will attend and give talks.
Two new interns will be starting this spring on topics related to their Master’s program (MPRI). Zakaria Chihani will be working on Proof certificates for some basic proof systems in classical logic. He will be starting 15 March 2012. Florence Clerc will be working on Relating double-negation translations and focused proof systems. She will be starting …
The book Programming with higher-order logic by Dale Miller and Gopalan Nadathur will be published by Cambridge University Press by the end of May 2012. It is available for pre-ordering on Amazon.com and Amazon.fr. The table of contents is available.
The following paper was accepted to QAPL 2012: A non-local method for robustness analysis of floating point programs by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Draft dated 3 Feb 2012 (HAL).