All about Proofs, Proofs for All
Overview
Many of us, logicians, work towards the improvement of proofs, proof systems, proof formats, interactive proof script languages, proof search methods... But what makes a proof (systemformatsearchmethod...) better than another? Logicians from different communities will give radically different answers to this question! The principles behind their answers may be unknown to outsiders; they may even sound obscure, ungrounded or in apparent contradiction to the principles of other communities.
The Vienna Summer of Logic presents a unique opportunity to promote a conversation between all the communities on questions related to proofs. ∀X.XΠ will promote a fruitful knowledge exchange by organizing short tutorials given by prominent speakers from various communities. These tutorials shall be accessible to young researchers and of interest to experienced researchers from other communities as well.
Preliminary Program
Slot  Topic  Speakers 

9:00  SATSolvers (paper, slides) 
Marijn Heule Marijn Heule is a Research Scientist at the University of Texas at Austin. He received his PhD at Delft University of Technology in the Netherlands in 2008. His research focusses on solving hard combinatorial problems in areas such as formal verification and number theory. Most of his contributions are related to practical satisfiability solving. He is one of the editors of the Handbook of Satisfiability and an associate editor of the Journal on Satisfiability, Boolean Modeling and Computation (JSAT). 
9:30  SMTSolvers (Satisfiability Modulo Theories) (paper, slides) 
Clark Barrett Clark Barrett is an Associate Professor of Computer Science at New York University. He received his PhD from Stanford University in 2003, advised by David Dill. His PhD thesis laid the groundwork for the architecture of modern Satisfiability Modulo Theories (SMT) solvers. He has written numerous articles on the subject and built several systems, the latest of which is CVC4. Professor Barrett was a founder of the SMT competition, and helps lead the SMTLIB initiative, an effort to create standards and develop resources for the SMT community. He received the IBM Software Quality Innovation Award in 2008 for CVC3, and he was the recipient of the Haifa Verification Conference award in 2010 for his pioneering work in SMT. Pascal Fontaine Pascal Fontaine is maître de conférences in Nancy at the University of Lorraine and he is affiliated to Inria for his research. He obtained his PhD from the University of Liège, Belgium, in 2004, and works in Nancy since then. In his early days as a researcher, he was involved in the development of the haRVey SMT solver. Lateron he initiated, together with David Déharbe, the development of the veriT SMT solver. In 2006, proof production for SMT solvers and proof reconstruction from SMT proofs started to capture his interest, as necessary mechanisms to make SMT technologies available in other tools. He is also concerned with proof representation and proof compression. Leonardo de Moura Leonardo de Moura is a Principal Researcher in the RiSE group at Microsoft Research. He joined Microsoft in 2006, before that he was a Computer Scientist at SRI International. His research areas include automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is a new open source theorem prover being developed from scratch. Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. He received the Haifa Verification Conference Award in 2010. In 2014, the Z3 tool paper received "The most influential tool paper in the first 20 years of TACAS" award. 
10:15  10:45 
Break 

10:45  FirstOrder Automated Theorem Provers (paper, slides) 
Stephan Schulz Stephan Schulz studied computer science at the University of Kaiserlautern. Parts of his undergraduate work on proof extraction, structuring, and presentation for the distributed equational prover DISCOUNT have survived through Waldmeister and now migrated into Mathematica. 
11:15  HigherOrder Automated Theorem Provers (paper, slides) 
Christoph Benzmüller In 2012, Christoph Benzmüller was awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG). In this position he is currently affiliated with Freie Universität Berlin, Germany, where he holds a venia legendi in Mathematics (and Computer Science). Previously, Christoph held positions as Full Professor for Artificial Intelligence and Formal Methods at the International University in Bruchsal, Germany, and as an Associate and Assistant Professor in Computer Science at Saarland University, Saarbrücken, Germany. Recently, Christoph received major international recognition for his research (jointly with Bruno WoltzenlogelPaleo) on the formalization and automation of Kurt Gödel's ontological argument for the existence of God on the computer. 
11:45  12:00 
Break 

12:00  Interactive Theorem Provers (paper, slides) 
Makarius Wenzel Makarius Wenzel is, together with Tobias Nipkow and Lawrence Paulson, one of the principal developers of the Isabelle theorem prover. In particular he is responsible for the design of the Isar structured proof language and the recent PIDE (jedit) interface. He has also been instrumental (with David Matthews) in increasing parallelism in Isabelle, to the point where it really speeds up interactive work in practice. But he is involved in almost all other aspects of the tool. 
12:30  Calculus of Inductive Constructions (paper, slides) 
Christine PaulinMohring Christine PaulinMohring is a Professor at Université ParisSud 11 since 1997. She obtained her PhD in 1989 from Université Paris 7, working under the supervision of Gérard Huet at INRIA Rocquencourt and Ecole Normale Supérieure on the early version of the Calculus of Constructions. She spent 8 years as a CNRS Researcher at Ecole Normale Supérieure in Lyon, where she contributed to the development of the Coq proof assistant especially on the aspects concerning inductive definitions and program extraction. She lead the research group ProVal (INRIA Saclay  ÎledeFrance, Université ParisSud and CNRS) until 2011, working on the use of proof technologies for developing correct programs. Her recent work includes the development of a Coq library ALEA to reason on randomized programs. 
13:00  14:30 
Lunch 

14:30  Foundational Proof Certificates (paper, slides) 
Dale Miller Dale Miller received his PhD in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and a department head at Pennsylvania State University. He has held visiting positions at the universities of AixMarseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research at INRIASaclay where he is the Scientific Leader of the Parsifal team. 
15:00  Deduction Modulo (paper, slides) 
Gilles Dowek Gilles Dowek is a researcher at Inria in the Deducteam team. He is interested in the formalization of mathematics (type theory, set theory, nominal logics, etc.), in proof processing systems (proofchecking, automated theorem proving, etc.), in the design of quantum programming languages and in the safety of aerospace systems. He is also a consultant for the National Institute of Aerospace, a lab of the NASA Langley research center. Among other things, he has participated to the development and the proof of ACCoRD, an Airborne Coordinated Conflict Resolution and Detection system. In the past, he has been a professor at École Polytechnique. More generally, he is interested in education and he tries to draw the attention of the administration to the need of introducing computer science in K12. Finally, he is also interested in the philosophy of sciences. 
15:30  Deep Inference (paper) 
Alessio Guglielmi Alessio Guglielmi is a proof theory researcher who teaches theoretical 
16:00  16:30 
Break 

16:30 
JeanRaymond Abrial JeanRaymond Abrial is the coinventor of various formal method approaches: Z, B and EventB. He is the author of the "Bbook" (CUP 1996), which presents the BMethod. He published recently a new book "Modeling in EventB: System and Software Engineering" (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform tool for EventB (funded by the European Project "Rodin"). After that, he was a researcher also at ETH Zurich, working on a new European Project called "Deploy" till May 2009. More recently, he is a consultant for another European Project: "Advance". He is also frequently invited in China giving some formal method courses in various Chinese Universities (Peking University in Beijing, East China Normal University in Shanghai). Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world. 

17:00  Security (paper, slides) 
Gilles Barthe Gilles Barthe is a professor at the IMDEA Software Institute since April 2008. His research interests include formal methods, programming languages and program verification, software and system security, and cryptography, and foundations of mathematics and computer science. Since 2006, he has been working on the development of formal verification tools for cryptography. 
17:30  Mathematical Proof Analysis (paper, slides) 
Alexander Leitsch Alexander Leitsch is professor of Mathematics and Theoretical Computer Science at the Vienna University of Technology. In 1974 he obtained his PhD in mathematics at the University of Vienna (with a thesis on probability theory). In 1985 habilitation at the University if Linz with a thesis on recursion theory. In 1986/1987 visiting associate professor at the CIS department of the University of Delaware. Since 1987 full professor at the Vienna University of Technology. In 2001 guest researcher at the CNRS in Grenoble (rank: directeur de recherche) for three months. Member of the editorial board of Studia Logica, program cochair of IJCAR in 2001. Research interests are computational proof theory and automated deduction. Books: The Resolution Calculus (1997), Automated Model Building (2004, with R. Caferra and N. Peltier), Methods of CutElimination (2011, with M. Baaz). 
Book
Each tutorial will be accompanied by a short paper. A collection of the papers will be published as a book by College Publications. A preliminary version of the book will be distributed to earlyregistered participants of the workshop.
Invited Speakers
 JeanRaymond Abrial
 Clark Barrett (New York University, USA)
 Gilles Barthe (IMDEA Software Institute, Madrid, Spain)
 Christoph Benzmüller (Freie Universität Berlin, Germany)
 Gilles Dowek (INRIA Paris, France)
 Pascal Fontaine (LORIA Nancy, France)
 Alessio Guglielmi (University of Bath, England)
 Marijn Heule (University of Texas at Austin, USA)
 Alexander Leitsch (Vienna University of Technology, Austria)
 Dale Miller (École Polytechnique, Paris, France)
 Leonardo de Moura (Microsoft Research, USA)
 Christine PaulinMohring (LRI & INRIA Saclay, France)
 Stephan Schulz (Munich University of Technology, Germany)
 Makarius Wenzel (LRI, Université Paris Sud, France)
Organization
 David Delahaye (Cedric/Cnam/Inria, Paris)  chair
 Bruno Woltzenlogel Paleo (Vienna University of Technology)  chair