Email Gateway (Aug 18 2022 at 18:01): Email Gateway (Aug 18 2022 at 18:01):From: Freek Wiedijk <freek@cs.ru.nl>
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@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
Last updated: Nov 21 2024 at 12:39 UTC