[TYPES/announce] ITP 2011 (Call for Participation)

Fri Jul 1 16:39:18 EDT 2011

				CALL FOR PARTICIPATION
      ITP 2011: 2nd International Conference on Interactive Theorem Proving
              22-25 August 2011, Nijmegen, The Netherlands
                     http://itp2011.cs.ru.nl/

                             -----

Important dates:
_____________

Early registration deadline: July 15th 2011 
Conference: 22-25 August 2011
Affiliated workshops: 26-27 August 2011

                            -----

Registration and Hotel
____________________

Registration open. Instruction on the ITP web-site:
http://itp2011.cs.ru.nl/ITP2011/Registration_-_Open.html

Hotel reservation is also open. Note the special rate of 60
Euros/night including breakfast. More information at:
http://itp2011.cs.ru.nl/ITP2011/Hotel_Reservation.html

                           -----

Conference
__________

ITP brings together researchers working in all areas of interactive
theorem proving.  It combines the communities of two venerable
meetings: the TPHOLs conference and the ACL2 workshop.  The inaugural
meeting of ITP was held on 11-14 July 2010 in Edinburgh, Scotland,
as part of the Federated Logic Conference (FLoC, 9-21 July 2010).
The second edition of ITP will take place in Nijmegen, The Netherlands, 
on 22-25 August 2011. 

The final programme will include 21 regular paper presentations and 4
rough diamonds presentations. It will also include 4 invited talks by
renown speakers from industry and academia. ITP 2011 has 8 affiliated
workshops. Submission to some workshops is still open. ITP will
finally feature two system demo's presenting the use of ACL2 and KeY on
large examples. This will give ITP experts the opportunity to get
insight into the practical use of two ITP systems.

This call for participations contain the list of accepter papers,
invited speakers, system demos, and affiliated workshops.

Accepted Papers
______________

David Monniaux and Pierre Corbineau. 
On the Generation of Positivstellensatz Witnesses in Degenerate Cases

Anthony Fox. 
LCF-style Bit-Blasting in HOL4

Johannes Hölzl and Armin Heller. 
Three Chapters of Measure Theory in Isabelle/HOL

Andreas Lochbihler and Lukas Bulwahn. 
Animating the Formalised Semantics of a Java-like Language

Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski and Lars Birkedal. 
Verifying object-oriented programs with higher-order separation logic in Coq

Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs and Jürgen Giesl. Termination of Isabelle Functions via Termination of Rewriting

Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest and Marc Cavazza. 
Structural Analysis of Narratives with the Coq Proof Assistant

Ondřej Kunčar. 
Proving Valid Quantified Boolean Formulas in HOL Light

Lennart Beringer. 
Relational decomposition

Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina. 
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials

Peter Gammie. 
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments

Scott Owens, Peter Boehm, Francesco Zappa Nardelli and Peter Sewell. 
Lightweight Tools for Heavyweight Semantics

Peter Reid and Ruben Gamboa. 
Automatic Differentiation in ACL2

Magnus O. Myreen and Jared Davis. 
A verified runtime for a verified theorem prover

Sylvain Heraud and David Nowak. 
A Formalization of Polytime Functions

Chunhan Wu, Xingyuan Zhang and Christian Urban. 
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions (Proof Pearl)

Renaud Clavel, Laurence Pierre and Regis Leveugle. 
Towards Robustness Analysis using PVS

Matej Urbas and Mateja Jamnik. 
Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers

Phil Scott and Jacques Fleuriot. 
Composable Discovery Engines for Interactive Theorem Proving

Tobias Nipkow. 
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism

Georges Gonthier. 
Point-free, set-free concrete linear alegbra

Tarek Mhamdi, Osman Hasan and Sofiene Tahar. 
Formalization of Entropy Measures in HOL

Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein. seL4 Enforces Integrity

Ramana Kumar and Tjark Weber. 
Validating QBF Validity in HOL4

Michael Norrish. 
Mechanised Computability Theory

Invited Speakers
_______________

Don Batory (UT Austin, USA)
Bart Jacobs (Radboud University Nijmegen)
Georges Gonthier (Microsoft)
Mike Kishinevsky (Intel)

Invited System Demos
______________________
ACL2 by Warren Hunt (UT Austin / Centaur)
KeY   by Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Peter H. Schmitt

Affiliated Workshops
___________________

** The third Coq workshop (Coq-3)
** http://www.cs.ru.nl/~spitters/coqw.html
Workshop day(s): August 26
Submission deadline:  May 16
Notification to authors: June 8

** The 6th International Workshop on Systems Software Verification
  (SSV'11)
** https://es.fbk.eu/events/ssv2011/index.php
Workshop day(s): August 26 
Submission deadline:  May 29
Notification to authors: June 30

** The ITP 2011 Workshop on Mathematical Wikis (MathWikis-2011)
** http://www.cs.ru.nl/mwitp/
Workshop day(s): August 27
Submission deadline:  May 30
Notification to authors: June 23

** The 3rd workshop on Modules and Libraries for Proof Assistans
  (MLPA-11)
** http://kwarc.info/frabe/events/mlpa-11/index.html
Workshop day(s): August 26
Submission deadline:  June 20 *********** submission still open ********************
Notification to authors: July 1

** The 3rd workshop on Dependently Typed Programming (DTP-11)
** http://www.cs.ru.nl/dtp11/
Workshop day(s): August 27
Submission deadline:  June 10 
Notification to authors: June 25
Contact: lfmtp2011 at easychair.org

** The 10th KEY Symposium (KeY-11).
** http://www.key-project.org/keysymposium11/
Workshop day(s): August 26 and 27

** The 6th International Workshop on Logical Frameworks and
**   Meta-languages: Theory and Practice (LFMTP-11)
** http://lfmtp11.cs.umn.edu/Site/Welcome.html
Workshop day(s): August 27
Submission deadline:  May 23
Notification to authors: June 22