.<html> <meta http-equiv="Content-Type" content="text/html; charset=utf-16"> <title>Concrete Semantics with Isabelle/HOL</title> <style type="text/css"> a:link { color: #4866FF; text-decoration: none } a:visited { color: #4866FF; text-decoration: none } a:active { color: #88A6FF; text-decoration: none } body { font-family: Geneva, Arial, Helvetica, sans-serif; color: #002164; background-color: white } </style> </html> <body> <table> <tr valign=top><td width=100> <font color="#dddddd" size=4> <td> <p align=right> <table> <tr> <td><a href="http://www.concrete-semantics.org/"><img src="book.jpg"></a> </table> </p> <h1>Concrete Semantics<br> with Isabelle/HOL</h1> <p><a href="http://people.mpi-inf.mpg.de/~jblanche/">Dr. Jasmin Blanchette</a> <br><a href="http://perso.eleves.ens-rennes.fr/~mfleur01/">Mathias Fleury</a> <br><a href="http://people.mpi-inf.mpg.de/~dwand/">Daniel Wand</a> <br> <br>Advanced course at Universit&auml;t des Saarlandes <br>6 credit points <br>Summer semester 2015 <br>&nbsp; <p>Contents:&nbsp; <a href="#material">Material</a> &sdot; <a href="#background">Background</a> &sdot; <a href="#resources">Resources</a> &sdot; <a href="#student_projects">Student Projects</a> &sdot; <a href="#exams_and_grades">Exams and Grades</a> &sdot; <a href="#contact">Contact</a> </p> <br> <a name="material"></a> <h2>Material</h2> <ul> <li><a href="slides.pdf">Main Slides</a>, <a href="slides_java.pdf">Java Slides</a>, <a href="Subtyping.thy">Subtyping Theory</a> <li>Exercise 1: <a href="ex01.pdf">Sheet</a> (28 April 2015), Solutions: <a href="sol01.thy">Exercises</a>, <a href="hwsol01.thy">Homework</a> <li>Exercise 2: <a href="ex02.pdf">Sheet</a> (4 May 2015), Solutions: <a href="sol02.thy">Exercises</a>, <a href="hwsol02.thy">Homework</a> <li>Exercise 3: <a href="ex03.pdf">Sheet</a> (11 May 2015), Solutions: <a href="sol03.thy">Exercises</a>, <a href="hwsol03.thy">Homework</a> <li>Exercise 4: <a href="ex04.pdf">Sheet</a> (18 May 2015), Solutions: <a href="sol04.thy">Exercises</a>, <a href="hwsol04.thy">Homework</a> <li>Exercise 5: <a href="ex05.pdf">Sheet</a> (1 June 2015), Solutions: <a href="sol05.thy">Exercise 1</a>, <a href="sol05_2.thy">Exercise 2</a>, <a href="hwsol05.thy">Homework</a> <li>Exercise 6: <a href="ex06.pdf">Sheet</a>, <a href="Van_Achternaam_Voornaam.thy">Template</a> (8 June 2015), Solutions: <a href="sol06.thy">Exercise</a>, <a href="hwsol06.thy">Homework</a> <li>Exercise 7: <a href="ex07.pdf">Sheet</a> (15 June 2015), Solutions: <a href="sol07_1.thy">Exercise 7.1</a>, <a href="sol07_2.thy">Exercise 7.2</a>, <a href="hwsol07.thy">Homework</a> <li>Exercise 8: <a href="ex08.pdf">Sheet</a>, <a href="Apellido_Primer_Nombre.thy">Template</a> (22 June 2015), Solutions: <a href="sol08_1.thy">Exercise 8.1</a>, <a href="sol08_2.thy">Exercise 8.2</a>, <a href="hwsol08.thy">Homework</a> <li>Exercise 9: <a href="ex09.pdf">Sheet</a>, <a href="Cognome_Prenome.thy">Template</a> (29 June 2015), Solutions: <a href="sol09.thy">Exercise</a>, <a href="hwsol09.thy">Homework</a> <li>Exercise 10: <a href="ex10.pdf">Sheet</a>, <a href="Myouji_Mei.thy">Template</a> (6 July 2015), Solutions: <a href="sol10.thy">Exercise</a> <li>Exercise 11: <a href="ex11.pdf">Sheet</a>, <a href="Patronymikos_Eponymikos.thy">Template</a> (20 July 2015), Solutions: <a href="sol11.thy">Exercise</a>, <a href="hwsol11.thy">Homework</a> <li>Exercise 12: <a href="ex12.pdf">Sheet</a>, <a href="Anonymous.thy">Template</a> (27 July 2015), Solutions: <a href="sol12.thy">Exercise</a> </ul> <br> <a name="background"></a> <h2>Background</h2> <p> This course introduces two topics together: <ul> <li>The first part is a self-contained introduction to the <b>proof assistant <a href="http://isabelle.in.tum.de/">Isabelle/HOL</a></b>. <li>The second part is an introduction to the <b>semantics of imperative programming languages</b>. This part is formalized in Isabelle. </ul> <p> This advanced course is based on a <a href="http://www.concrete-semantics.org/">brand new book</a> by <a href="http://www21.in.tum.de/~nipkow/">Prof. Tobias Nipkow</a> and <a href="http://www.cse.unsw.edu.au/~kleing/">Prof. Gerwin Klein</a>, which is available both as a free PDF online and as a hardcover from Springer. The material is complementary to the core <a href="https://www.ps.uni-saarland.de/courses/sem-ws13/">Semantics</a> course by <a href="https://www.ps.uni-saarland.de/~smolka/">Prof. Gert Smolka</a>, which uses Coq and focuses on the &lambda;-calculus and functional programming. <p> Proof assistants are tools that allow its users to carry out mathematical proofs rigorously, based on a logical foundation. Developing a proof in a proof asssistant as opposed to using pen and paper is roughly the equivalent of programming on a computer as opposed to sketching pseudocode on paper. Expertise with proof assistants is becoming an increasingly important skill, especially for software verification, which aims at <em>proving</em> the absence of bugs in programs. In the experience of many instructors, the use of a proof assistant helps students get a good grip on computer science topics. <p> Coq and Isabelle are the main two proof assistants in use. Isabelle's strength is that it is simple as 1-2-3: It offers (1)&nbsp;a simple yet powerful logic, (2)&nbsp;a convenient user interface, and (3)&nbsp;a lot of proof automation. <p>There are no formal prerequisites for taking the course. Familiarity with a typed functional programming language (such as Standard ML, OCaml, Haskell, or F#), as taught in <a href="http://www.cs.uni-saarland.de/index.php?id=225">Programmierung 1</a>, is highly recommended. <!-- <p> Here are a few good reasons to attend this course: <ol> <li> You enjoyed Prof. Smolka's lectures and would like to learn more about interactive theorem proving, program semantics, or both. <li> You missed Prof. Smolka's lectures but would still like to learn about interactive theorem proving, program semantics, or both. <li> You want to develop special skills that will make your Lebenslauf stand out. <li> You want to learn to make puns on the names of proof assistants. <li> You need the credit points. </ol> --> <p> <table border=0 cellpadding=0 cellspacing=0> <tr><td align=left>Lectures:&nbsp; <td align=right>Monday 10:15 to 11:45, E1 5, 6th floor, Seminarraum <br><tr><td align=left>Tutorials:&nbsp; <td align=right> Tuesday 10:15 to 11:45, E1 5, 6th floor, Seminarraum </table> <p> Topics: <ol> <li>Programming and Proving in Isabelle <li>Case Study: Expressions in a Programming Language <li>Logic and Proof beyond Equality <li>Isar: A Language for Structured Proofs <li>A Small Imperative Language <li>A Compiler <li>Types <li>Program Analysis <li>Denotational Semantics <li>Hoare Logic <li>Abstract Interpretation </ol> </p> <br> <a name="resources"></a> <h2>Resources</h2> <p> The <a href="http://www.concrete-semantics.org/">Concrete Semantics</a> web site lists the most important resources for this course. It also includes the demo files presented in the lectures (e.g., <tt>Overview_Demo.thy</tt>). </p> <p> The course is based on Isabelle2014. Beware: There are two user interfaces for Isabelle: Proof General and jEdit. We assume jEdit in this course. Proof General support will be discontinued in Isabelle2015, which is expected to be released in May or June 2015. </p> <p> The official <a href="http://isabelle.in.tum.de/documentation.html">Isabelle documentation</a> more details for those who are curious. In particular: <ul> <li><b>prog-prove</b> corresponds roughly to Part~I of the <em>Concrete Semantics</em> book. <li><b>tutorial</b> tells a more comprehensive story. Section 5, &ldquo;The Rules of the Game&rdquo;, is useful if you want to write detailed proofs, without appealing to sophisticated tactics. <li><b>main</b> is a summary of what's included in the basic <tt>Main</tt> theory. </ul> </p> <p> There's a vibrant <a href="https://isabelle.in.tum.de/community/Main_Page">community</a> around Isabelle, with mailing lists, wikis, etc. </p> <p> Higher-order logic (HOL) is a fairly simple (and weak) logic, which we will learn by doing. Those who are curious and want to know the whole story can look at the <a href="http://hol.sourceforge.net/documentation.html">HOL System LOGIC</a> manual, which is part of the documentation of the HOL4 proof assistant. </p> <br> <a name="student_projects"></a> <h2>Student Projects</h2> <p>Overall, 18 formalization projects were submitted by students as answers to exercise sheet 10. A few of them are collected below, with their authors' permission. </p> <ul> <li>Alexander Bentkamp: <a href="bentkamp_project.tgz">Hall and Latin Square</a> <li>Felix Freiberger: <a href="freiberger_project.tgz">Bisimilarity and CCS</a> <li>Fabian Kosmale: <a href="kosmale_project.thy">CCS and Bisimilarity</a> </ul> <br> <a name="exams_and_grades"></a> <h2>Exams and Grades</h2> <p> Credits and grades will be based on homework (including Isabelle developments) and a final written exam. The homework counts for 40% of the grade; the exam for 60%. </p> <p> The final exam will take place on 10 August 2015 from 14:00 to 16:00 in E1 3, HS 002. If necessary, a repeat exam is scheduled for 28 September 2015 from 14:00 to 16:00 in E1 5, 6th floor, Seminarraum. </p> <br> <a name="contact"></a> <h2>Contact</h2> <p> You can reach us at <a href="mailto:jasmin.blanchetteSPIDERMONKEYmpi-inf.mpg.de">jasmin.blanchetteSPIDERMONKEYmpi-inf.mpg.de</a> and <a href="mailto:mathias.fleurySPIDERMONKEYmpi-inf.mpg.de">mathias.fleurySPIDERMONKEYmpi-inf.mpg.de</a> if you have questions. Please put <tt>[CONCRETE]</tt> somewhere in the subject line. We will also be happy to answer your questions in person, but because the main instructor is co-located at Inria Nancy, it is a good idea to request an appointment by email. </p> <br> <br> <br> <p align=right>&ldquo;It is blatantly clear<font color=white>&rdquo;</font><br>You stupid machine, that what<font color=white>&rdquo;</font><br>I tell you is true.&rdquo;</p> <p align=right>&mdash; Michael Norrish<font color=white>&rdquo;</font></p><br> <p align=right>&ldquo;Hah! A proof of False.<font color=white>&rdquo;</font><br>Your axioms are bogus.<font color=white>&rdquo;</font><br>Go back to square one.&rdquo;</p> <p align=right>&mdash; Lawrence C. Paulson<font color=white>&rdquo;</font></p> <!-- http://www.cl.cam.ac.uk/research/hvg/haiku.html --> <br> <br> </body>