[Hol-info] Second Summer School on Formal Techniques, May 27-June 1, 2012
Second Summer School on Formal Techniques May 27- June 1, 2012 Menlo College, Atherton, CA http://fm.csl.sri.com/SSFT12 Formal verification techniques such as model checking, satisfiability, and static analysis have matured rapidly in recent years. This school, the second in the series, will focus on the principles and practice of formal verification, with a strong emphasis on the hands-on use and development of this technology. It primarily targets graduate students and young researchers who are interested in using verification technology in their own research in computing as well as engineering, biology, and mathematics. Students at the school will have the opportunity to experiment with the tools and techniques presented in the lectures. The first Summer Formal school (SSFT11; http://fm.csl.sri.com/SSFT11) was held in May 2011. This year, the school starts on Sun May 27 with a background course on Logic in Computer Science taught by Natarajan Shankar (SRI). The course is optional but highly recommended - it covers the prerequisites for the main lectures. We have NSF support for the travel and accommodation for students from US universities, but welcome applications from graduate students at non-US universities as well. Non-US students will have to cover their travel and lodging expenses (around $500). The deadline for applications is April 30. Non-US students requiring US visas are requested to apply early (by April 15). Interested students can submit their application at http://fm.csl.sri.com/SSFT12 The lecturers at the school include Leonardo de Moura (MSR Redmond) and Bruno Dutertre (SRI): Satisfiability Modulo Theories Sumit Gulwani (MSR): Dimensions in Program Synthesis Daniel Kroening (Oxford): Verifying Concurrent Programs Ken McMillan: Abstraction, Decomposition, and Relevance Corina Pasareanu, Dimitra Giannakopoulou, Neha Rungta, Peter Mehlitz, and Oksana Tkachuk: Verifying Components in the Right Context The school will also include invited talks by distinguished researchers. The SSFT Steering Committee consists of Tom Ball (MSR Redmond), Lenore Zuck (UIC), and Natarajan Shankar (SRI). -- This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CFP: CPP 2012 - 2nd International Conference on Certified Programs and Proofs
The Second International Conference on Certified Programs and Proofs (CPP 2012) CALL FOR PAPERS Kyoto, Japan December 13-15 2012 http://cpp12.kuis.kyoto-u.ac.jp/ co-located with APLAS 2012 http://aplas12.kuis.kyoto-u.ac.jp/ CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. The first CPP conference was held in Kenting, Taiwan during December 7-9, 2011. As with the first meeting, we plan to publish the proceedings in Springer-Verlag's Lecture Notes in Computer Science series. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; teaching mathematics and computer science with proof assistants; and Proof Pearls (elegant, concise, and instructive examples). IMPORTANT DATES: Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). Abstract Deadline: Friday, June 8, 2012 Paper Submission Deadline: Friday, June 15, 2012 Author Notification: Monday, August 27, 2012 Camera Ready:Monday, September 17, 2012 Conference: December 13-15, 2012 PROGRAM CO-CHAIRS: Chris Hawblitzel (Microsoft Research Redmond) Dale Miller(INRIA Saclay and LIX, Ecole Polytechnique) GENERAL CHAIR: Jacques Garrigue (Nagoya University) PROGRAM COMMITTEE: Stefan Berghofer (Technical University Munich) Wei-Ngan Chin (National University of Singapore) Adam Chlipala (MIT) Mike Dodds (University of Cambridge) Amy Felty (University of Ottawa) Xinyu Feng (University of Science and Technology of China) Herman Geuvers (Radboud University, Nijmegen) Robert Harper (Carnegie Mellon University) Chris Hawblitzel (Microsoft Research Redmond) Gerwin Klein (NICTA) Laura Kovacs (Vienna University of Technology) Dale Miller(INRIA Saclay and LIX, Ecole Polytechnique) Rupak Majumdar (UCLA, Max Planck Institute for Software Systems) Lawrence Paulson (University of Cambridge) Frank Piessens (KU Leuven) Randy Pollack (Harvard and Edinburgh University) Bow-Yaw Wang (Academia Sinica) Santiago Zanella Béguelin (IMDEA Software Institute) ORGANIZING COMMITTEE: Jacques Garrigue and Atsushi Igarashi Email: cpp201...@math.nagoya-u.ac.jp CPP STEERING COMMITTEE: Andrew Appel (Princeton University) Nikolaj Bjørner (Microsoft Research Redmond) Georges Gonthier (Microsoft Research Cambridge) John Harrison (Intel Corporation) Jean-Pierre Jouannaud (co-Chair) (INRIA and Tsinghua University) Gerwin Klein (NICTA) Tobias Nipkow (Technische Universität München) Zhong Shao (co-Chair) (Yale University) SUBMISSION INSTRUCTIONS: Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2012 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness,
[Hol-info] Quick and easy exchange of ML values via XML/YXML
Dear HOL users, in the old LISP days, exchange of symbolic data was really trivial, using built-in read/write functions for s-expressions. Later things became more complex in ML, and especially with XML. The following tiny library in SML or OCaml makes things again mostly trivial: https://bitbucket.org/makarius/yxml/src/ YXML is pronounced Why XML. It is both the question and answer to the problem of concrete transfer syntax of seemingly trivial tree expressions. The other part is a rather obvious combinator library to represent typed ML expressions over untyped XML, in the same spirit as the ML runtime would do that for untyped bits in memory. Isabelle/ML has included both as standard library functions for quite some time already. Maybe the independent versions above help to bridge over to other provers from the HOL family. Makarius -- This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] congruence theorems for partial higher-order functions
Is it possible to get good termination condition extraction for functions like listTheory$MAP2? I can prove something like this: |- ∀l1 l1' l2 l2' f f'. (l1 = l1') ∧ (l2 = l2') ∧ (LENGTH l1 = LENGTH l2) ∧ (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (f x y = f' x y)) ⇒ (MAP2 f l1 l2 = MAP2 f' l1' l2') But it's probably of the wrong form (because of the condition about the lengths being equal), and indeed adding it to the database in DefnBase doesn't help with termination condition extraction for uses of MAP2. Without a condition like that, though, I think the congruence is unprovable. Is there a right form? -- This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
