Dale Miller

Team leader of Parsifal. My postal address and other contact information are:

INRIA Saclay & LIX, Bât. Alan Turing	phone: +33 (0)1 77 57 80 53
1 rue Honoré d'Estienne d'Orves
Campus de l'École Polytechnique	email: dale.miller at inria.fr
91120 Palaiseau, France

My office is room 2053. Instructions to get to the Alan Turing building. The time and weather in Paris.

Programming with Higher-Order Logic

The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012.

See my list of papers and talks, my CV (html, pdf), a brief bio, and my academic genealogy.

ACM Transactions on Computational Logic: Editor-in-chief and Area editor for Proof Theory. Instructions for submitting to ToCL.
Journal of Automated Reasoning: Member of the Editorial Board.
Journal of Applied logic: Scientific Area Editor. Elsevier.
Theory and Practice of Logic Programming: Advisory Board member. Cambridge University Press.

Keywords: Computational logic, programming language theory, proof theory, proof certificates, linear logic, automated deduction.

Funded programs: ProofCert: Broad Spectrum Proof Certificates, an ERC Advanced Investigator Grant funded for the five years 2012-2016. Also: Eternal, Structural, RAPT.

I am supervising one internship ("stages") during spring and summer 2013. I regularly lecture at MPRI (Master Parisien de Recherche en Informatique) in the Course 2-1: Logique linéaire et paradigmes logiques du calcul. In recent years, I have also taught graduate courses at the Universities of Pisa (September 2011), Milan (March 2010), and Ca' Foscari Venezia (April 2009). My current PhD students are Ivan Gazeau and Zakaria Chihani. I have supervised a number of PhD and MS students.

CADE 2013: The 24th International Conference on Automated Deduction, Lake Placid, New York, 9-14 June. Accepted paper.
LICS 2013: The Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, 25-28 June 2013, New Orleans. Accepted paper.
Tableaux 2013, Nancy, France, 16-19 September 2013. Program Committee member.
LFMTP 2013: Logical Frameworks and Meta-Languages: Theory and Practice, Boston, 22 September 2013. Invited speaker.
FICS 2013, Fixed Points in Computer Science, 1 September 2013, Torino. Steering committee.
CPP 2013, Certified Programs and Proofs, Melbourne, Australia, December 2013 (colocated with APLAS 2013). Steering committee.
LIX Colloquium 2013, The Theory and Applications of Formal Proofs, Palaiseau France. 12-15 November 2013 (colocated with PSATTT 2013). Organizing committee.
In the summer of 2014, CSL and LICS will be held as a single, joint conference with the name Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL14) and the 29th ACM / IEEE Symposium on Logic in Computer Science (LICS14) during 14-18 July 2014. This joint meeting will have one PC and one proceedings. Tom Henzinger and I will be the Program Committee Chairs. This conference will be part of FLoC 2014 which, in turn, is part of the Vienna Summer of Logic.

A photo of me is here and at the end of this album. I am married to Catuscia Palamidessi and we have two children: Nadia and Alexis. Some humor for mid-day distractions.