Topics for Internships

Dale Miller is proposing the following internship for 2010.

1. Towards a broad spectrum proof certificate.

Completed internships

• Model Checking as Deduction. Completed by Ivan Gazeau in 2009. Gazeau is currently a PhD student in the Parsifal and Comete teams.
• Proving theorems about logic specifications. Completed by Alexandre Viel in 2008. Viel is currently a PhD student in the Parsifal team.
• Formal connections between various asynchronous specification languages. Completed by David Baelde in 2006: report is available as PS. Baelde completed his PhD in Parsifal in 2008.
• Congruence of bisimulation in higher-order and mobile process calculi. Completed by Axelle Zieger in 2005. Later she published the following paper based on this internship: A congruence format for name-passing calculi, by Axelle Ziegler, Dale Miller, and Catuscia Palamidessi. In the proceedings of SOS05: Structural Operational Semantics.