<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
        {font-family:Consolas;
        panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0in;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
span.EmailStyle17
        {mso-style-type:personal-compose;
        font-family:"Calibri","sans-serif";
        color:windowtext;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-family:"Calibri","sans-serif";}
@page WordSection1
        {size:8.5in 11.0in;
        margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
        {page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">The deadline for submitting to CPP 2012 is June 8, 2012.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; The Second International Conference on<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Certified Programs and Proofs (CPP 2012)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; CALL FOR PAPERS<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Kyoto, Japan<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; December 13-15 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; http://cpp12.kuis.kyoto-u.ac.jp/<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; co-located with APLAS 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; http://aplas12.kuis.kyoto-u.ac.jp/<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">CPP is a new international forum on theoretical and practical topics<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">in all areas, including computer science, mathematics, and education,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">that consider certification as an essential paradigm for their work.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Certification here means formal, mechanized verification of some sort,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">preferably with production of independently checkable certificates.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">We invite submissions on topics that fit under this rubric.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">The first CPP conference was held in Kenting, Taiwan during December<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">7-9, 2011. As with the first meeting, the proceedings will be<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">published in Springer-Verlag's Lecture Notes in Computer Science<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">series.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Suggested, but not exclusive, specific topics of interest for<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">submissions include: certified or certifying programming, compilation,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">linking, OS kernels, runtime systems, and security monitors; program<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">logics, type systems, and semantics for certified code; certified<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">decision procedures, mathematical libraries, and mathematical<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">theorems; proof assistants and proof theory; new languages and tools<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">for certified programming; program analysis, program verification, and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">proof-carrying code; certified secure protocols and transactions;<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">certificates for decision procedures, including linear algebra,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">polynomial systems, SAT, SMT, and unification in algebras of interest;<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">certificates for semi-decision procedures, including equality,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">first-order logic, and higher-order unification; certificates for<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">program termination; logics for certifying concurrent and distributed<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">programs; higher-order logics, logical systems, separation logics, and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">logics for security; teaching mathematics and computer science<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">with proof assistants; and &quot;Proof Pearls&quot; (elegant, concise, and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">instructive examples).<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">IMPORTANT DATES:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Authors are required to submit a paper title and a short abstract<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">before submitting the full paper. The submission should include when<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">necessary a url where to find the formal development assessing the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">essential aspects of the work. All submissions will be electronic.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">All deadlines are at midnight (GMT).<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Abstract Deadline:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Friday, June&nbsp; 8, 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Paper Submission Deadline:&nbsp;&nbsp; Friday, June 15, 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Author Notification:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Monday, August 27, 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Camera Ready:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Monday, September 17, 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Conference:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; December 13-15, 2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">PROGRAM CO-CHAIRS:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Chris Hawblitzel&nbsp;&nbsp; (Microsoft Research Redmond)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Dale Miller&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (INRIA Saclay and LIX, Ecole Polytechnique)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">GENERAL CHAIR:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Jacques Garrigue&nbsp;&nbsp; (Nagoya University)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">PROGRAM COMMITTEE:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Stefan Berghofer&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (secunet Security Networks AG)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Wei-Ngan Chin&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(National University of Singapore)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Adam Chlipala&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (MIT)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Mike Dodds&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (University of Cambridge)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Amy Felty&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (University of Ottawa)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Xinyu Feng&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (University of Science and Technology of China)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Herman Geuvers&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Radboud University, Nijmegen)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Robert Harper&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Carnegie Mellon University)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Chris Hawblitzel&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Microsoft Research Redmond)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Gerwin Klein&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (NICTA)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Laura Kovacs&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Vienna University of Technology)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Dale Miller&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (INRIA Saclay and LIX, Ecole Polytechnique)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Rupak Majumdar&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (UCLA, Max Planck Institute for Software Systems)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Lawrence Paulson&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (University of Cambridge)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Frank Piessens&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (KU Leuven)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Randy Pollack&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Harvard and Edinburgh University)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Bow-Yaw Wang&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Academia Sinica)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Santiago Zanella Béguelin&nbsp; (IMDEA Software Institute)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">ORGANIZING COMMITTEE:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Jacques Garrigue and Atsushi Igarashi<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Email: cpp2012oc@math.nagoya-u.ac.jp<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">CPP STEERING COMMITTEE:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Andrew Appel&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Princeton University)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Nikolaj Bjørner&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Microsoft Research Redmond)&nbsp;&nbsp;
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp;&nbsp;Georges Gonthier&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Microsoft Research Cambridge)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; John Harrison&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Intel Corporation)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Jean-Pierre Jouannaud (co-Chair)&nbsp; (INRIA and Tsinghua University)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Gerwin Klein&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (NICTA)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Tobias Nipkow&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(Technische Universität München)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">&nbsp; Zhong Shao (co-Chair)&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Yale University)
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">SUBMISSION INSTRUCTIONS:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Papers should be submitted electronically online via the conference<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">submission web page at URL:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">http://www.easychair.org/conferences/?conf=cpp2012<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Acceptable formats are PostScript or PDF, viewable by Ghostview or<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Acrobat Reader. Submissions should not exceed 16 pages in LNCS format,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">including bibliography and figures. Submitted papers will be judged on<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">the basis of significance, relevance, correctness, originality, and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">clarity. They should clearly identify what has been accomplished and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">why it is significant. The proceedings of the symposium will be<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">published as a volume in Springer-Verlag&#8217;s Lecture Notes in Computer<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Science series.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Each submission must be written in English and provide sufficient<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">detail to allow the program committee to assess the merits of the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">paper. It should begin with a succinct statement of the issues, a<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">summary of the main results, and a brief explanation of their<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">significance and relevance to the conference, all phrased for the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">non-specialist. Technical and formal developments directed to the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">specialist should follow. Whenever appropriate, the submission should<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">come along with a formal development, using whatever prover, e.g.,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Vampire, etc. References and comparisons with related work should be<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">included. Papers not conforming to the above requirements concerning<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">format and length may be rejected without further consideration.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">The results must be unpublished and not submitted for publication<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">elsewhere, including the proceedings of other published conferences<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">or workshops. The PC chairs should be informed of closely related work<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">submitted to a conference or journal in advance of submission.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">Original formal proofs of known results in mathematics or computer<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">science are among the targets. One author of each accepted paper is<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-size:9.5pt;font-family:Consolas;color:black;background:white;mso-highlight:white">expected to present it at the conference.<o:p></o:p></span></p>
<p class="MsoNormal"><o:p>&nbsp;</o:p></p>
</div>
</body>
</html>